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

Karl Palmskog (Feb 08 2022 at 02:21):

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

Daniel Hilst Selli (Feb 08 2022 at 02:50):

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: Apr 20 2024 at 14:01 UTC