I'm trying to implement a simple lambda calculus eval function in Coq here is what I have so far

```
From Coq Require Import Strings.String.
Inductive expr :=
| Var : string -> expr
| Lamb : string -> expr -> expr
| Appl : expr -> expr -> expr.
Inductive context :=
| NilContext : context
| Context : string -> expr -> context -> context.
Fixpoint lookup (key : string) (ctx : context) : option expr :=
match ctx with
| NilContext => None
| Context str expr ctx' =>
if (str =? key)%string
then Some expr
else lookup key ctx'
end.
Fixpoint eval (ctx : context) (e : expr) {struct e} : expr :=
match e with
| Var x =>
match lookup x ctx with
| Some y => eval ctx y
| None => Var x
end
| Appl e1 e2 =>
let e1' := eval ctx e1 in
let e2' := eval ctx e2 in
match e1' with
| Lamb x body =>
let ctx := Context x e2' ctx in
eval ctx body
| _ => Appl e1 e2
end
| Lamb x body => Lamb x body
end.
```

`eval`

function is ill-formed because I'm calling it on result of `lookup`

so I have the classical `Recursive call to eval has principal argument equal to "y" instead of a subterm of "e".`

What is the right way to solve this?

there is no canonical way, you'll have to use some mechanism that allows encoding recursion with measures/well-foundedness proofs (or equivalent), such as `Program Fixpoint`

or Equations. I'd recommend making `context`

into a regular `list`

first though.

Something like `list (string * expr)`

?

right

Any material about well-foundedness, I tried CPDT chapter and failed to grasp it :/

if you have access to the Coq'Art book (example code at https://github.com/coq-community/coq-art), it has several chapters on well-foundedness and general recursion.

Otherwise, this could be helpful: https://coq.discourse.group/t/fixpoint-with-two-decreasing-arguments/544/4

Thank you Karl!

Wait, why well-foundedness ? This is untyped lambda calculus evaluation, so it is not terminating.

You probably want to use fuel instead.

Well-founded recursion doesn't help for terminating lambda calculi either.

@Daniel Hilst Selli and sorry for the unsolicited advice, but there might be some correctness issues with this interpreter... Would you want to hear, or find out yourself?

If you are thinking about alpha-conversion, it should be fine, since the evaluator never dives under binders.

doesn't it? on `App (Lamb x (Var x)) (Var x)`

it will push `x := Var x`

to the context, evaluate `Var x`

, discover that `x`

is bound to `Var x`

, and continue evaluating in the same context so loop

I was attempting to not say yet, since it might be part of the learning experience :grinning:

Gaëtan Gilbert said:

doesn't it? on

`App (Lamb x (Var x)) (Var x)`

it will push`x := Var x`

to the context, evaluate`Var x`

, discover that`x`

is bound to`Var x`

, and continue evaluating in the same context so loop

Do you have an example with a closed term?

Okay, "evaluate result of lookup" was indeed the first issue

And at this point: without closures, this can only implement dynamic scoping.

Hello Paolo, I want to hear if you don't mind

I see, now that Gaëtan said it feels obvious :thinking:

Last updated: Jun 15 2024 at 05:01 UTC