Non-trivial recursive function: how to prove recursion is well-founded?

Using Coq
1

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 well_founded?

2

Recursive occurrences of a fixpoint must be applied to a subterm of its decreasing argument. Here in op f t, f is not applied to anything.

This would probably be accepted if you replace the op parameter with subst , because it unfolds to applications of cont (that is f) to subterms of t.

It is also common to have to rephrase “pen and paper” definitions so they’re easier to formalize in Coq. The definition you gave translates to three somewhat overlapping match expressions. You can do it with a single match, at the cost of a little more verbose definition in English.

  fix f t :=
    match t with
    | Var n => Var n
    | (\ t1) $$ t2 => subst (f t1) (f t2)
    | t1 $$ t2 => f t1 $$ f t2
    | \t' => \(f t')
    end.