Termination proof of term rewriting system with the multiset path ordering. A complete development in the system Coq

We show how to incorporate rewriting into the Calculus of Constructions and we prove that the resulting system is strongly normalizing with respect to beta and rewrite reductions. An important novelty of this paper is the possibility to define rewriting rules over dependently typed function symbols. We prove strong normalization for any term rewriting system, such that all function symbols satisfy the, so called, star dependency condition, and every rule is accepted by the Higher Order Recursive Path Ordering (which is an extension of the method created by Jouannaud and Rubio for the setting of the simply typed lambda calculus). The proof of strong normalization is done by using a typed version of reducibility candidates due to Coquand and Gallier. Our criterion is general enough to accept definitions by rewriting of many well-known higher order functions, for example dependent recursors for inductive types or proof carrying functions. This makes it a very good candidate for inclusion in a proof assistant based on the Curry-Howard isomorphism.

Download Full-text

LEARNING FROM EXAMPLES IN UNIVERSE OF DISCOURSE DESCRIBED BY A SET OF EQUATIONS

International Journal of Artificial Intelligence Tools ◽

10.1142/s0218213092000235 ◽

1992 ◽

Vol 01 (03) ◽

pp. 333-350

Author(s):

EMMANUEL KOUNALIS

Keyword(s):

Background Knowledge ◽

Term Rewriting ◽

Learning From Examples ◽

Implicit Representation ◽

Term Rewriting System ◽

Rewriting System ◽

Finite Set ◽

Formal Basis ◽

Knowledge Problem ◽

Universe Of Discourse

Generalization is an important operation for programs that learn. Anti-unification guarantees the existence of a term which is the most specific generalization of a collection of terms. This provides a formal basis for learning from examples. However, such generalization may be "too" general and therefore counterexamples are required to restrict them. In this case, the learner has to check whether the resulting formula provides a concept to learn, i.e. whether a formula of the form t/{t1,…,tn} is a generalization, where t is viewed as a generalization of a set of examples and t1,…,tn are counterexample. The formula t/{t1,…,tn} is often called an implicit representation. The implicit representation t/{t1,…,tn} is a generalization iff there exist ground (variable-free) instances of t which are not instances of t1,…,tn. This is a non-trivial task even when there is no background knowledge (see [15]). We present here a method to check whether an implicit representation t/{t1,…,tn} is a generalization with respect to a finite set of equations which describes the background knowledge problem, i.e. whether there exists a ground instance of t which is not equivalent to any ground instance of t1,…,tn with respect to a set E of equations. Whereas this problem is in general undecidable since the equality is so, we show in this paper that in this case where the set E of equations is compiled into a ground convergent term rewriting system, we can discover concepts in Universe of Discourse with background knowledge described by a finite set of equations. We show how the method applies to induce concepts in theories of elementary arithmetic.

Download Full-text

HANDLING NON LEFT-LINEAR RULES WHEN COMPLETING TREE AUTOMATA

International Journal of Foundations of Computer Science ◽

10.1142/s0129054109006917 ◽

2009 ◽

Vol 20 (05) ◽

pp. 837-849 ◽

Cited By ~ 1

Author(s):

YOHAN BOICHUT ◽

ROMEO COURBIS ◽

PIERRE-CYRILLE HEAM ◽

OLGA KOUCHNARENKO

Keyword(s):

General Problem ◽

Transitive Closure ◽

Term Rewriting ◽

Tree Automata ◽

Regular Model ◽

Term Rewriting System ◽

Rewriting System ◽

Regular Model Checking ◽

Successor Relation ◽

Tree Languages

This paper addresses the following general problem of tree regular model-checking: decide whether [Formula: see text] where [Formula: see text] is the reflexive and transitive closure of a successor relation induced by a term rewriting system [Formula: see text], and [Formula: see text] and [Formula: see text] are both regular tree languages. We develop an automatic approximation-based technique to handle this – undecidable in general – problem in the case when term rewriting system rules are non left-linear.

Download Full-text

Calculation of Fundamental Groups via Computational Paths

10.5753/etc.2021.16370 ◽

2021 ◽

Author(s):

T. M. L. de Veras ◽

A. F. Ramos ◽

R. J. G. B. de Queiroz ◽

A. G. de Oliveira

Keyword(s):

Projective Plane ◽

Term Rewriting ◽

Fundamental Groups ◽

Real Projective Plane ◽

The Real ◽

Term Rewriting System ◽

Rewriting System

We address the question as to how to formalise the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. The intention is to demonstrate the use of a term rewriting system in performing computations with these computational paths, establishing equalities between equalities, and further higher equalities, in particular, in the calculation of fundamental groups of surfaces such as the circle, the torus and the real projective plane.

Download Full-text