I am trying to formalize the Church-Rosser theorem for the untyped-lambda calculus. There are actually multiple such theorems, depending on whether one is considering only beta-reduction, or beta- and eta-reduction, or something more exotic. I would like my implementation to be parameterized so that I can reuse it across different reduction modalities.
I am following Selinger’s lecture notes, which explains the classic proof due to Tait and Martin-Löf. The step on page 35 is to implement the maximal one-step parallel reduction operation.
This operation can be explained as follows: if the term under examination is amenable to the reduction(s) being considered (eta, beta, both, …) then first recurse on the subterms, and then perform a reduction on the result. Otherwise, immediately recurse on the subterms.
Implementing this in such a way that the reduction is pluggable requires passing a callback to the reduction function. Here is a sketch implementation for beta reduction:
(* Perform beta reduction, and call the continuation on the resulting subterms.*) Definition subst (cont: Term -> Term) (t: Term): option Term := match t with | (\t1) $$ t2 => Some(subst (cont t1) (cont t2)) | _ => None end. Section reduction. Hypothesis op: (Term -> Term) -> Term -> option Term. Definition maximal_parallel_reduction: Term -> Term := fix f (t: Term) := match op f t with | Some t' => t' | None => match t with | Var n => Var n | t1 $$ t2 => (f t1) $$ (f t2) | \t' => \(f t') end end. End reduction.
Now Coq’s checks for well-founded recursion don’t agree with the call
op f t. I’ve never had to deal with non-trivial recursion in Coq. Is my best guess to work with