## Stream: Coq users

### Topic: lambda calculus eval in Coq

#### Daniel Hilst Selli (Feb 08 2022 at 02:13):

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?

#### Karl Palmskog (Feb 08 2022 at 02:16):

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.

#### Daniel Hilst Selli (Feb 08 2022 at 02:20):

Something like `list (string * expr)`?

right

#### Daniel Hilst Selli (Feb 08 2022 at 02:30):

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

#### Karl Palmskog (Feb 08 2022 at 02:34):

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!

#### Paolo Giarrusso (Feb 08 2022 at 08:41):

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

#### Paolo Giarrusso (Feb 08 2022 at 08:42):

You probably want to use fuel instead.

#### Paolo Giarrusso (Feb 08 2022 at 08:48):

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

#### Paolo Giarrusso (Feb 08 2022 at 08:51):

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

#### Guillaume Melquiond (Feb 08 2022 at 08:53):

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

#### Gaëtan Gilbert (Feb 08 2022 at 08:58):

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

#### Paolo Giarrusso (Feb 08 2022 at 08:58):

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

#### Guillaume Melquiond (Feb 08 2022 at 08:59):

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?

#### Paolo Giarrusso (Feb 08 2022 at 08:59):

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

#### Paolo Giarrusso (Feb 08 2022 at 09:00):

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

#### Daniel Hilst Selli (Feb 08 2022 at 09:21):

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

#### Daniel Hilst Selli (Feb 08 2022 at 09:23):

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

Last updated: Jun 15 2024 at 05:01 UTC