TRS: Term Rewriting and Abstract Reduction Systems Theories
For PVS 6.0
Last updated: 16 March 2019.
Mauricio Ayala Rincon
Universidade de Brasilia
Brazil
ayala@unb.br
Andre Luiz Galdino
Universidade de Brasilia &
Campus Catalao/Universidade Federal de Goias
Brazil
galdino@catalao.ufg.br
Contains a unification theory developed by both authors together with
Andreia Borges Avelar
Universidade de Brasilia
Brazil
avelarab@gmail.com
Contains a orthogonality theory developed by two first authors together with
Ana Cristina Rocha Oliveira Valverde
Universidade de Brasilia
Brazil
anacrismarie@gmail.com
Contains a Innermost Dependency Pairs theory developed by the first author and
Ariane Alves Almeida
Universidade de Brasilia
Brazil
arianealvesalmeida@gmail.com
1. Package Files
----------------
a. README Summary of distribution (this file)
b. The folder "trs-pvs60" which contains the ARS and TRS theories
-------------------------------------------------------------------
b.1. ARS theories
-----------------
relations_closure.pvs This theory contains the definitions of closure
of a relation and some properties.
ars_terminology.pvs This theory contains some terminology of ARS such
as unique normal form, reducible and sucessor, and
notions of confluence and commutation.
results_confluence.pvs This theory contains some results about confluence
such as strong confluent implies semi-confluent.
results_commutation.pvs This theory contains some results about commutation
such as Commutation lemma.
results_normal_form.pvs This theory contains some results involving normal
form such as a relation is normalizing and
confluent iff every element has a unique
normal form.
noetherian.pvs This theory contains the definition of convergent
reduction and noetherian relation and the
Noetherian induction lemma.
newman_yokouchi.pvs This theory contains the specification of Newman's
lemma and Yokouchi's lemma
modulo_equivalence.pvs This theory contains specifications about Reduction
modulo equivalence such as local confluence, confluence
and Church-Rosser property modulo equivalence, and some
properties such as the general newman's lemma.
confluence_commute.pvs This theory contains some results and exercises from
the book TeReSe.
b.2. TRS theories
-----------------
arity.pvs This theory contains the definition of the function
arity.
term.pvs This theory contain the definition of an abstract term
structure.
variables_term.pvs This theory contain the definition of a variable set V.
term_adt.pvs This theory is automatically generated by the
specification of a term (term.pvs) and contains
extensionality axioms, eta axiom, induction scheme and
a well-foundedness axiom.
positions.pvs This theory contains the definitons of the set of
positions of a term, parallel positions among other,
and some properties of positions.
subterm.pvs This theory contains the notions of subterm of a term,
and variables occurring in a term, and some properties.
replacement.pvs This theory contains the definition of replacing the
subterm at some position by a term, and some properties.
compatibility.pvs This theory contains the definitions of closed under
substitutions and operations, and compatible with
operations and contexts, and some properties such as
compatible with operations iff compatible with contexts.
substitution.pvs This theory contains the definitions of substitution,
domain and range of a substitution, restriction and
extention of a substitution, composition of two
substitutions, and a most general unifier,
and some properties.
extending_rename.pvs This theory contain the definition that extend a rename
from a given domain to the same type as identity.
rewrite_rules.pvs This theory contains the definitions of a rewrite rule
and a set (type) of rewrite rules.
reduction.pvs This theory contains the definition of reduction
relations (at some position and restricted to non-root position)
and some properties such as closed under
substitutions and compatible with operations.
replace_positions.pvs This theory contains the notion of substitutes all
subterms at a sequence of parallel positions of a term
by another term, and some properties.
unification.pvs This theory is composed of a set of specifications and
formalization of definitions and lemmas which allowed us
to formalize the lemma which guarantee the existence of
a most general unifier on set first-order terms.
robinsonunification.pvs This theory contains the formalization of a greedy
first-order unification algorithm a la Robinson.
robinsonunificationEF.pvs This theory contains the formalization of a more
efficient first-order unification algorithm a la
Robinson.
critical_pairs_aux.pvs This theory contains definitions and properties needful
to prove the Critical Pairs Theorem.
critical_pairs.pvs This theory contains the definition of a Critical Pairs
and the Critical Pairs Theorem.
orthogonality_basis.pvs This theory contains specification of notions related
to orthogonal rewriting systems, parallel rewriting, the
formalization of confluence of left and right linear
non-ambiguous TRSs and the Parallel Moves Lemma.
orthogonality_sets.pvs This theory contains the proof of the Theorem of
confluence of orthogonal TRSs. The inductive proof of
the main theorem uses the Parallel Moves Lemma. In this
version, sequences (of rules, variables, terms,
substitutions) involved in one-step parallel rewritings
and parallel forks, are translated into sets in order to
avoid direct treatment of these sequences, using instead
simpler set properties.
orthogonality.pvs This theory also contains the proof of the Theorem of
confluence of orthogonal TRSs. The inductive proof of
the main theorem uses the Parallel Moves Lemma. Some
operators over sequences of positions are used and,
differently from the theory orthogonality_sets, no
advantage of properties over sets is exploited.
predicate_fseq2set.pvs This theory states several properties of finite
sequences over a non interpreted type T converted in
sets through the PVS prelude conversions "seq2set" and
"set2seq".
IUnion_extra.pvs This theory contains additional properties about
disjoint sets operations and finite union of a finite
family of finite sets.
top.pvs This theory imports the theories trs,
robinsonunificationEF, orthogonality and
orthogonality_sets.
seq_extras.pvs This theory was developed by the two first authors but
it was realloced to the 'structures' folder of NASA
Langley PVS Libraries in the current version. Until the
version 5.0, the theory was named as
finite_sequences_extras.pvs and it was in 'TRS' folder.
It contains definitions and properties about finite
sequences.
seq_recursion_theorem This theory contains a version of the recursion theorem
for set theory, allowing the construction of functions
over the naturals to elements of a non-empty set/predicate
for which there exists a function over elements of such
set/predicate. This result is used to build infinite
chains of Dependency Pairs from a minimal non-terminating
term. Despite its application it is a general set theoretical
result.
restricted_reduction This theory contains a definition allowing to restrict a given
relation to the descendants of a given element. It also contains
results for noetherianity of such relations. Also used in the
Dependency Pairs Theory.
innermost_reduction This theory contains the definition of innermost reduction
relations (at some position and restricted to non-root position)
and some properties such as closed under
substitutions and compatible with operations.
dependency_pairs This theory contains the formalization of the correction
of the (innermost) Dependency Pairs termination criterion.
2. REQUIREMENTS
---------------
a. Make sure PVS 6.0 has been installed.
Available at: http://pvs.csl.sri.com/
b. trs theory requires NASA Langley PVS Libraries which are available at:
http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/
These libraries should be included.
------------------------