Define a type Variable of metavariables.

Template: data Variable = …

Write a type FOOpenTerm of first-order open terms (essentially rose trees where branches represent functions and leaf nodes represent metavariables and constants, and a constant is just a 0-ary function). This type should have one type parameter: a type of function symbols.

Template: data FOOpenTerm (fun ∷ ⋆) = …

Write a new type FOTerm that is like FOOpenTerm, but parameterized over an arbitrary type of metavariables, so that you can represent closed terms by setting the parameter to Void.

Template: data FOTerm (fun ∷ ⋆) (var ∷ ⋆) = …

Write a new type HOTerm, that is like FOTerm, but it supports binder nodes, which can capture variables. Assume that each binder node can only capture one variable. The type of binders should be a parameter; for example, the lambda calculus would have data Binder = Lam as the parameter, whereas first-order logic would have data Binder = ForAll | Exists as the parameter.

Template: data HOTerm (fun ∷ ⋆) (var ∷ ⋆) (binder ∷ ⋆) = …

Redefine FOOpenTerm and FOTerm as type aliases in terms of HOTerm.

Write a function that computes the set of free variables in an HOTerm.

Template: freeVars ∷ (Ord v) ⇒ HOTerm f v b → Set v

Implement capture-avoiding substitution of a single variable on HOTerms.

Template: subst ∷ (v, HOTerm f v b) → HOTerm f v b → HOTerm f v b

Implement capture-avoiding simultaneous substitution on HOTerms.

Template: simulSubst ∷ [(v, HOTerm f v b)] → HOTerm f v b → HOTerm f v b

Write a type HOSubst of substitutions in terms of HOTerm (essentially a partial function from variables to terms).

Template: data HOSubst (fun ∷ ⋆) (var ∷ ⋆) (binder ∷ ⋆) = …

Redefine simulSubst in terms of your type of substitutions.

Template: simulSubst ∷ HOSubst f v b → HOTerm f v b → HOTerm f v b

Define a type alias FOSubst of substitutions on first-order terms in terms of HOSubst.

Implement syntactic unification (using the Robinson algorithm or the Martelli-Montanari algorithm) on FOTerms.

Template: unify ∷ FOTerm f v → FOTerm f v → Maybe (FOSubst f v)

A transition system is a pair (S, →) of a set of states S and a transition relation (→) ⊆ S². A labelled transition system is a triple (S, Λ, →) where (→) ⊆ (S × Λ × S).

A term-rewriting system (TRS) is a transition system whose set of states is given by a set of terms, and whose transition relation is given by a set of rewrite rules, which, for our purposes, will be pairs p ↦ e where p is a pattern (FO open) term and e is an expression (FO open) term, and the set of free variables in e is a subset of the set of free variables in p.

If (a, b) is a pair of terms in a TRS, we say that a derives b (denoted a →* b) when there exists a finite sequence of rewrites that starts at a and ends with b. In other words, →* is the reflexive-transitive closure of the → relation. Similarly, the transitive closure of → is denoted by →⁺.

A pair of terms (a, b) in a TRS is joinable (denoted a ↑ b) iff there exists a term c such that a →* c and b →* c.

A pair of terms (a, b) in a TRS is meetable iff there exists a term c such that c →* a and c →* b.

A TRS is locally confluent if for every triple of terms (a, b, c) such that a → b and a → c, there exists a term d such that b →* d and c →* d.

A TRS is confluent (or satisfies the Church-Rosser property) if for every triple of terms (a, b, c) such that a →* b and a →* c, there exists a term d such that b →* d and c →* d.

Without referring to any outside resources (spoilers are easy to find), come up with a term-rewriting system that is locally confluent but not confluent.

Extra credit: come up with a term-rewriting system that has no cycles (when thought of as a digraph) that is locally confluent but not confluent.

Write a type Rule f v for first-order rewrite rules.

We can apply a rewrite rule p ↦ e to a term t by unifying p with t to get a substitution θ, and then applying θ to e.

Write a function that does this.

Template: applyRule ∷ Rule f v → FOTerm f v → Maybe (FOTerm f v)

Write a type TRS f v for first-order term-rewriting systems in terms of Rule. A term-rewriting system cannot contain the same rule twice.

Write a type LTRS f v l for labelled first-order term-rewriting systems. The l parameter is for the type of labels.

Rewrite TRS f v as a type alias for LTRS f v ().

Write a function that computes the set of terms that are the result of applying a rewrite rule to a given term.

Template: oneStepTRS ∷ TRS f v → FOTerm f v → Set (FOTerm f v)

Generalize the oneStepTRS function to the LTRS type.

Template: oneStepLTRS ∷ (Ord f, Ord v) ⇒ LTRS f v l → FOTerm f v → Map (FOTerm f v) l

We can compute the set of terms derivable from a given term in a TRS by doing a breadth-first search using oneStepLTRS. The search may not terminate so the output should be given through a callback. The callback will take the current rule (the node in the search tree) and the list of rule labels used so far (the path from the root to the current node in the search tree).

Template: forDerivable ∷ (Monad m) ⇒ LTRS f v l → FOTerm f v → (FOTerm f v → [l] → m a) → m ()

A critical pair in a term-rewriting system is a pair of terms (t₁, t₂) such that there exists a term t for which two different applications of a rewrite rule (either the same rule applied differently, or two different rules) yield the terms t₁ and t₂.

More precisely, to compute the set of critical pairs of a term-rewriting system, we do the following for every (not necessarily distinct) pair of rules r₁ = (p₁ ↦ e₁) and r₂ = (p₂ ↦ e₂):

• Simultaneously (i.e.: with the same substitution) rename the variables in p₂ and e₂ so that the set of free variables of r₂ is disjoint from that of r₁.

• For each non-variable subterm s in p₁, try unifying s with p₂. If unification succeeds, assume it returns a substitution θ (if it fails, continue on in the loop).

  Denote the application (i.e.: simultaneous substitution) of θ to a term t by θ(t).

  Define x to be θ(e₁). Define y to be the result of replacing every instance of θ(s) in θ(p₁) with θ(e₂).

  Yield the critical pair (x, y) and continue the loops.

Implement this algorithm for the TRS type.

Template: criticalPairs ∷ TRS f v → Set (FOTerm f v, FOTerm f v)

A critical pair is convergent iff it is joinable. If all the critical pairs of a term-rewriting system are convergent, then it is locally confluent.

Write a program, using criticalPairs and forDerivable, that automatically checks if a given term-rewriting system is locally confluent. Do not worry about the efficiency of the algorithm. It should terminate if the given term-rewriting system is strongly-normalizing, but it may not if that is not the case.

Template: isLocallyConfluent ∷ TRS f v → Bool

Implement the Knuth-Bendix completion algorithm, which computes a confluent and terminating TRS with the same deductive closure as the input TRS. The algorithm may not terminate. Try it on some simple TRSes: a theory with only ground terms (no variables), the theory of monoids of size n, the theory of groups of size n.

Template: knuthBendix ∷ TRS f v → TRS f v