Infinitary Rewriting in Coq

A Coq formalisation of infinitary rewriting.

Introduction

This is an attempt at formalising the basic notions from infinitary term rewriting in the Coq proof assistant, in a way that is natural for Coq (using dependent types and (co)induction). For more information, see my Master thesis on this project below.

Together with the thesis, this formalisation constitutes my Master project, roughly a six months project concluding my Master in theoretical computer science at the VU University Amsterdam.

Relevant literature can be found on my CiteULike page.

Coq code

The code was developed using Coq version 8.3 beta0-1 and version 8.3 rc1. I intend to test for compatibility with Coq 8.3 shortly after its release.

Download version 1.2, 2010-09-01: infinitary-rewriting-1.2.tar.gz

Or get the latest development version from GitHub.

Or browse the code online from the coqdoc index. Roughly in order of dependence, the development consists of the following libraries:

Prelims.v

Some preliminaries.

Vector.v

Dependently typed (by their lenth) lists.

Signature.v

A signature is a decidable set of function symbols.

Variables.v

A decidable set of variables.

FiniteTerm.v

Terms over a signature and a set of variables.

Term.v

Infinite terms over a signature and a set of variables.

TermEquality.v

Bisimilarity and pointwise equality on infinite terms.

Substitution.v

Substituting terms for variables in terms.

Context.v

Infinite contexts over a signature and a set of variables.

ContextEquality.v

Bisimilarity and pointwise equality on infinite contexts.

Ordinal.v

Ordinal numbers represented as tree ordinals.

WfOrdinal.v

Well-formed tree ordinals.

Rewriting.v

Definition of a TRS, rewrite steps, and transfinite rewrite sequences.

ExampleABA.v

A small example of an infinitary term rewriting system.

NoUniqueNormalFormsWO.v

A counterexample to the unique normal forms property in weakly orthogonal systems.

NoUniqueNormalFormsWOElaborated.v

Some additional lemmas on the counterexample.

Master thesis

This thesis describes our formalisation of the basic notions from the theory of infinitary term rewriting in the Coq proof assistant. Infinitary term rewriting is a generalisation of term rewriting where we allow terms to be infinitely deep and admit rewrite sequences of transfinite length. Coq is an interactive proof assistant based on constructive type theory with inductive types. The main contribution of our formalisation is an inductive definition of transfinite rewrite sequences, based on tree ordinals.

The ordinal numbers are represented by tree ordinals, following the construction of an order on tree ordinals by Hancock (2008). Infinite terms are defined by coinduction. A novel representation for rewrite sequences of ordinal length is defined, based on the inductive structure of the tree ordinals. The order on ordinals is then lifted to an embedding relation on rewrite sequences. We discuss an application of our formalisation in the verification of a counterexample to unique normal forms in weakly orthogonal infinitary TRSs, introduced by Endrullis, Grabmayer, Hendriks, Klop, and van Oostrom (2010).

Infinitary Rewriting in Coq. MSc thesis, VU University Amsterdam, 2010.

Author

Martijn Vermaat (martijn@vermaat.name)

License

Licensed under the MIT license.