The Coq mailing list

[Donald Leung <i.donaldl AT me.com>]

Dear coq-clubbers,

I have recently been looking into the untyped lambda calculus (UTLC) and its 
formalization in Coq which lead to a question about the properties of a 
verified beta-reduction evaluator for said calculus. But first, some 
background: suppose we define the syntax of lambda terms in the UTLC as 
follows:

```coq
Inductive tm : Type :=
  | Var : nat -> tm      (* deBruijn index *)
  | App : tm -> tm -> tm (* M N *)
  | Abs : tm -> tm.      (* \. M *)
```

Then lifting and substitution (as defined in Iron Lambda: 
http://iron.ouroborus.net):

```coq
Fixpoint lift (depth : nat) (term : tm) : tm :=
  match term with
  | Var n => if lt_dec n depth then Var n else Var (S n)
  | App M N => App (lift depth M) (lift depth N)
  | Abs M => Abs (lift (S depth) M)
  end.

Fixpoint subst (depth : nat) (u term : tm) : tm :=
  match term with
  | Var n =>
      match lt_eq_lt_dec n depth with
      | inleft (left _) => Var n
      | inleft (right _) => u
      | inright _ => Var (n - 1)
      end
  | App M N =>
      App (subst depth u M) (subst depth u N)
  | Abs M =>
      Abs (subst (S depth) (lift 0 u) M)
  end.
```

And single-step beta reduction, using evaluation contexts (again, following 
the style of Iron Lambda):

```coq
Inductive eval_ctx : (tm -> tm) -> Prop :=
  | eval_ctx_top :
      eval_ctx (@id tm)
  | eval_ctx_app_left : forall N,
      eval_ctx (fun M => App M N)
  | eval_ctx_app_right : forall M,
      eval_ctx (App M)
  | eval_ctx_abs :
      eval_ctx Abs.

(* Single-step beta reduction *)

Inductive beta_step : tm -> tm -> Prop :=
  | beta_step_subst : forall M N,
      beta_step (App (Abs M) N) (subst 0 N M)
  | beta_step_ctx : forall C term term',
      eval_ctx C ->
      beta_step term term' ->
      beta_step (C term) (C term').
```

Notice that our single-step beta-reduction relation is nondeterministic. Now, 
I have been able to implement and prove correct a single-step beta-reduction 
evaluator which returns Some t’ if the given lambda term can take a step to 
t’, and None otherwise:

```coq
Parameter beta_step_eval : tm -> option tm.
```

It has been proven correct in the sense that 1) it only ever performs valid 
beta-reduction steps and 2) it is always able to reduce lambda terms with 
beta-redexes:

```coq
(* Our beta single-step evaluator only performs valid
   beta-reduction steps *)

Axiom beta_step_eval_sound : forall t t',
  beta_step_eval t = Some t' ->
  beta_step t t'.

(* Our beta single-step evaluator is always able to reduce
   lambda terms with beta-redexes *)

Axiom beta_step_eval_complete : forall t t',
  beta_step t t' ->
  exists t'', beta_step_eval t = Some t''.
```

Now, define the multi-step beta-reduction relation to be the reflexive, 
transitive closure of `beta_step`:

```coq
From Coq Require Import Relations.

Definition beta_multistep : tm -> tm -> Prop :=
  clos_refl_trans_1n tm beta_step.
```

It is easy to implement a multi-step beta-reduction evaluator based on some 
gas parameter `n` which performs at most `n` beta-reduction steps based on 
`beta_step` (implementation elided):

```coq
Parameter beta_multistep_eval : nat -> tm -> tm.
```

To show that this multi-step evaluator is correct, we could first prove that 
it only performs valid beta-reduction steps similar to what we did for our 
single-step evaluator, which follows directly by induction on the gas 
parameter (proof elided):

```coq
Axiom beta_multistep_eval_sound : forall gas t t',
  beta_multistep_eval gas t = t' ->
  beta_multistep t t'.
```

However, this property alone is not enough to show that our implementation of 
`beta_multistep_eval` is correct, because the trivial implementation that 
never performs any beta-reduction steps also satisfies this property (by 
matching the `rt1n_refl` constructor unconditionally):

```coq
Definition beta_multistep_eval (_ : nat) (t : tm) : tm := t.
```

I have not been able to come up with a property analogous to 
`beta_step_eval_complete` for the multi-step evaluator. Are there any 
properties other than `beta_multistep_eval_sound` above relating 
`beta_multistep` and `beta_multistep_eval` that successfully differentiates a 
proper implementation of `beta_multistep_eval` from the trivial 
implementation shown above? Any ideas would be much appreciated.

Yours sincerely,
Donald

P.S. I was thinking of stating and proving that our multistep evaluator 
always reduces a lambda term to some beta-normal form within a finite number 
of steps given that the lambda term has a beta-normal form, something like:

```coq
Theorem beta_multistep_eval_complete : forall t t',
  beta_multistep t t' ->
  beta_normal_form t' ->
  exists gas, beta_multistep gas t = t'.
```

However, it occurred to me this morning that even if a lambda term in the 
UTLC has a beta-normal form, certain choices of reduction steps may still 
fail to terminate, implying that a multi-step evaluator may not always choose 
the correct reduction steps to reach a beta-normal form for a lambda term, 
provided that there is one. Or is it possible to implement the evaluator in 
such a way that it always chooses the correct reduction steps towards a 
beta-normal form (if exists)?