The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

A term that cannot reduce is sometimes called "stuck" (some people only call "stuck" the terms that are not values). The ability to keep reducing is sometimes called "progress". So instead of "completeness", maybe you could use "progress".

Note that you could formulate crisper statements if your evaluator exposed a more informative API. For example, you could have an

    eval : nat -> term -> term * bool

such that:

1. (eval n t) is (u, true) if t reduces to u in exactly n steps,

2. (eval n t) is (u, false) if t reduces to u in (k < n) steps and u is stuck.

Proving (1) and (2) above would capture both your soundness and completeness/progress statements.

On Sun, Feb 9, 2020 at 4:16 PM Donald Leung <i.donaldl AT me.com> wrote:

Thanks Li-yao and Gabriel for your input, I will definitely take a look into call-by-name evaluation.

As for my ill-named “completeness” theorem, what might be a better name for said theorem, or is my theorem rather nonstandard?

~ Donald

Gabriel Scherer <gabriel.scherer AT gmail.com>於2020年2月9日 22:56寫道：

Dear Donald,

Yes, there are results on the fact that some reduction strategies are guaranteed to terminate if a normal-form exists (call-by-name is one such strategy, and is simple to define). Conversely, there are "maximal" reduction strategies that are such that, if there exists a n-long reduction chain, then the strategy can do at least n reductions.

A natural analogue of your one-step "completeness" result would be that if a n-long reduction chain exists (instead of (beta_multistep t t') you would define (beta_multistep n t t'), counting the number of one-step reductions), then the evaluator will perform n reductions. However, this is not true of all sensible evaluators: some may find an irreducible value in less than n steps.

I think that "completeness" is not a good name for the (one- or multi-)step statement that you are writing. We say that an computational description of a system is "complete" with respect to a more declarative presentation if the computations can perform everything allowed by the spec (and "sound" if it always respects the declarative presentation). In your setting I would expect completeness to mean that *any* relation ({one,multi}step_beta t t') can be turned into an equality (eval {,n} t = t'), which is not true.

You don't get very strong results because your relational and algorithmic presentation do not match each other very well. You could change them to match better, and thus get a real completeness statement (any reduction relation is realized by computation):

- You could change your reduction relation to enforce a given evaluation strategy, for example as left-to-right call-by-value, matching your evaluator.

- You could change your evaluator to be non-deterministic (for example in monadic style) and perform all possible reductions, matching your reduction relation.

On Sun, Feb 9, 2020 at 12:25 PM Donald Leung <i.donaldl AT me.com> wrote:

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