Introduction
------------

This package provides an effective version of infinitary term rewriting,
as described in "Computing with Infinite Terms and Infinite Reductions"
by Jeroen Ketema and Jakob Grue Simonsen.

The Haskell code in this package has been tested with version 8.0.2 of
the Glasgow Haskell Compiler (GHC). To obtain GHC, it is best to install
the Haskell Platform:

  http://hackage.haskell.org/platform/

Usage
-----

To experiment, execute the interpreter supplied with GHC (ghci) with either:

* IntroductionExample.hs  (for the example from the Introduction),
* CompressionExamples.hs  (for the compression theorem),
* ConfluenceExamples.hs   (for the confluence theorem), or
* ChurchRosserExamples.hs (for the Church-Rosser property).

Then, input the examples as described in the comments of the .hs files.

Structure
---------

The code has been split in several files whose contents should be mostly
obvious from the file names, or otherwise from the initial comments in
each of the files.

Note that there are a few minor differences compared to the paper:

* Signatures are sets with an arity function instead of sets of pairs.
* Terms are represented by a recursive data type instead of partial functions.
* Rewrite systems are objects with a rule function instead of a rule set.
* The implementation of Lemma 8.4 does not compute needed reductions to avoid
  duplicating computation of these reductions, instead these reductions are
  passed in as parameters.
* To avoid clutter, rewrite systems are omitted as input parameters except in
  the top-level functions defining compression, the Strip Lemma, confluence,
  and the Church-Rosser property.
* In several places only the steps of finite reductions are passed instead
  of both a sequence of terms and a sequence of steps. Steps suffice in these
  places.
* Extraction of steps from a computably strongly convergent reduction exploits
  the fact that the assumed systems of notation have a less then or equal
  operator. As reductions are usually represented by lists, this leads to
  slightly more efficient code: Instead of having to work backwards through a
  list of steps from some ordinal determined by the modulus we can go forwards
  (see "select" in SystemOfNotation.hs).

Correspondence with the Paper
-----------------------------

The correspondence between the Turing machines defined in the the paper and
the functions as present in the code is as follows:

Example 3.6      : rationalTerm          in RationalTerm.hs
Lemma 3.10       : substitute            in Substitution.hs
Proposition 3.12 : subterm               in PositionAndSubterm.hs
Lemma 4.2        : rewriteStep           in RuleAndSystem.hs
Remark 5.6       : ordLimitPred          in SystemOfNotation.hs
Remark 5.10      : finalTerm             in Reduction.hs
Proposition 7.4  : descendantsAcrossStep in RuleAndSystem.hs
Lemma 7.7        : origins               in Reduction.hs
Lemma 7.11       : neededSteps           in Reduction.hs
Lemma 7.12       : descendants           in Reduction.hs
Proposition 7.16 : neededReduction       in Reduction.hs
Proposition 8.3  : limitedPermute        in ParallelReduction.hs
Lemma 8.4        : filterSteps           in ParallelReduction.hs
Lemma 8.5        : parallelNeededSteps   in ParallelReduction.hs
Lemma 8.6        : diamondProperty       in ParallelReduction.hs
Theorem 9.1      : compression           in Compression.hs
Theorem 10.1     : confluence            in Confluence.hs
Lemma 10.2       : stripLemma            in StripLemma.hs
Lemma 10.4       : confluenceSide        in Confluence.hs
Theorem 10.5     : churchRosser          in ChurchRosser.hs
Lemma 10.6       : interleave            in ChurchRosser.hs

(End of README)