Stream: Coq users

Topic: lambda calculus eval in Coq


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Daniel Hilst Selli (Feb 08 2022 at 02:20):

Something like list (string * expr)?

view this post on Zulip Karl Palmskog (Feb 08 2022 at 02:21):

right

view this post on Zulip Daniel Hilst Selli (Feb 08 2022 at 02:30):

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

view this post on Zulip 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

view this post on Zulip Daniel Hilst Selli (Feb 08 2022 at 02:50):

Thank you Karl!

view this post on Zulip Paolo Giarrusso (Feb 08 2022 at 08:41):

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

view this post on Zulip Paolo Giarrusso (Feb 08 2022 at 08:42):

You probably want to use fuel instead.

view this post on Zulip Paolo Giarrusso (Feb 08 2022 at 08:48):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Feb 08 2022 at 08:59):

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

view this post on Zulip Paolo Giarrusso (Feb 08 2022 at 09:00):

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

view this post on Zulip Daniel Hilst Selli (Feb 08 2022 at 09:21):

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

view this post on Zulip Daniel Hilst Selli (Feb 08 2022 at 09:23):

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


Last updated: Jan 27 2023 at 00:03 UTC