Summary

The file proof.zip contains a Coq proof of the termination of the reading and merging rules in the suspension calculus. This work is based on the proof given in A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi by Andrew Gacek and Gopalan Nadathur. To test this proof simply unpack the archive and execute 'make test' within it.

The Coq development is split into two files. The first, Susp.v, defines expressions and rewriting in the suspension calculus and the second, RPO.v, defines a recursive path ordering on suspension expressions which is proven to decrease when a term is rewritten. A detailed description of important element of these files is given below.

Detailed Description

The first half of the proof is contained in Susp.v which begins by defining the syntactic categories of terms and environments which are coalesced into a single category called term. The reading and merging rules schemas are defined in the predicate rm which holds between two terms when the first rewrites to the second by a rule application at the top level. This predicated is generalize to the step predicate which corresponds to . Next the measures mu and eta are defined as in the paper. The main result of this half of the development is then proved in the theorem eta_step which states that if t rewrites to t' in one step then eta of t is greater than or equal to eta of t'.

The second half of the proof is contained in RPO.v which begins by defining the abstract representation of terms introduced in the paper. The vocabulary of symbols discussed in the paper is represented by symbol and the corresponding ordering    is defined as slt. The category of terms is then defined in term and the recursive path ordering is defined in rpolt. Finally, the translation is defined in E. The primary result of this development is the theorem step_rpolt which states that if t rewrites to t' in one step then the translation of t is greater than the translation of t' under the recursive path ordering. Given the existing literature on recursive path orderings mentioned in the paper, this means the reading and merging rules in the suspension calculus are terminating.

Acknowledgements

This material is based upon work supported by the National Science Foundation under Grants CCR-0429572 and OISE-0553462 (IRES-REUSSI). Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.