help with proof of equiv of small and big step eval in UTLC

Stream: general

[Paige Thomas]

I'm trying to prove that if the reflexive transitive closure of the small step call by name evaluation of an untyped lambda calculus expression holds then the big step evaluation holds; that is, one direction of showing that they are equivalent. I have a proof of the other direction. I was wondering if someone might see a way forward with the proof, or what I might be doing wrong? I haven't yet found a proof in the literature, or at least not one I can follow, or in mathlib. I hope to do the same for call by value, normal order, and applicative order.

import Mathlib.Logic.Relation


@[reducible]
def Symbol_ : Type := String
deriving Inhabited, DecidableEq, Repr


inductive Expr_ : Type
| Var : Symbol_ → Expr_
| App : Expr_ → Expr_ → Expr_
| Lam : Symbol_ → Expr_ → Expr_
deriving Inhabited, DecidableEq, Repr


def is_lam_expr
  (M : Expr_) :
  Prop :=
  ∃ (x : Symbol_) (e : Expr_), M = Expr_.Lam x e


inductive is_bn_small_step
  (sub : Symbol_ → Expr_ → Expr_ → Expr_) :
  Expr_ → Expr_ → Prop
| rule_1
  (e1 e1' e2 : Expr_) :
  is_bn_small_step sub e1 e1' →
  is_bn_small_step sub (Expr_.App e1 e2) (Expr_.App e1' e2)

| rule_2
  (x : Symbol_)
  (e1 e2 : Expr_) :
  is_bn_small_step sub (Expr_.App (Expr_.Lam x e1) e2) (sub x e2 e1)


inductive is_bn_big_step
  (sub : Symbol_ → Expr_ → Expr_ → Expr_) :
  Expr_ → Expr_ → Prop
| rule_1
  (x : Symbol_) :
  is_bn_big_step sub (Expr_.Var x) (Expr_.Var x)

| rule_2
  (x : Symbol_)
  (e : Expr_) :
  is_bn_big_step sub (Expr_.Lam x e) (Expr_.Lam x e)

| rule_3
  (x : Symbol_)
  (e e' e1 e2 : Expr_) :
  is_bn_big_step sub e1 (Expr_.Lam x e) →
  is_bn_big_step sub (sub x e2 e) e' →
  is_bn_big_step sub (Expr_.App e1 e2) e'

| rule_4
  (e1 e1' e2 : Expr_) :
  ¬ is_lam_expr e1' →
  is_bn_big_step sub e1 e1' →
  is_bn_big_step sub (Expr_.App e1 e2) (Expr_.App e1' e2)


example
  (sub : Symbol_ → Expr_ → Expr_ → Expr_)
  (M N : Expr_)
  (h1 : Relation.ReflTransGen (is_bn_small_step sub) M N) :
  is_bn_big_step sub M N :=
  by
    induction h1
    case refl =>
      induction M
      case Var x =>
        apply is_bn_big_step.rule_1
      case App e1 e2 ih_1 ih_2 =>
        induction e1 generalizing e2
        case Var e1_x =>
          apply is_bn_big_step.rule_4
          · unfold is_lam_expr
            simp
          · apply is_bn_big_step.rule_1
        case App e1_e1 e1_e2 e1_ih_1 e1_ih_2 =>
          apply is_bn_big_step.rule_4
          · unfold is_lam_expr
            simp
          · exact ih_1
        case Lam e1_x e1_e e1_ih_1 =>
          apply is_bn_big_step.rule_3
          · exact ih_1
          · sorry
      case Lam x e ih_1 =>
        apply is_bn_big_step.rule_2
    case tail N'' N' ih_1 ih_2 ih_3 =>
      induction M generalizing N'' N'
      case Var x =>
        cases ih_3
        cases ih_2
      case App e1 e2 ih_4 ih_5 =>
        cases N''
        case Var N''_x =>
          cases ih_2
        case App N''_e1 N''_e2 =>
          sorry
        case Lam N''_x N''_e =>
          cases ih_2
      case Lam x e ih_4 =>
        cases ih_3
        cases ih_2

[Paige Thomas]

Maybe this doesn't hold, or is missing some condition?

[Bhavik Mehta]

I don't think this holds, even in the reflexive case; App (Lam "x" (Var "x")) (Var "y") doesn't big-step reduce to itself. It should even be true that big-step reduction can't produce an unreduced applied lambda expression

[Paige Thomas]

Did I translate the big step reduction definition wrong? I took it from 6.1 here: https://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf

[Shreyas Srinivas]

Small step reductions refine big step reductions, not the other way around. This means if you have a big step reduction, then there is a corresponding small step reduction with the same start and end points

[Shreyas Srinivas]

Small step reductions allow terms to reduce in non-terminating ways

[Shreyas Srinivas]

You can define big step reductions to avoid all that, though I don't see that happening in your setup

[Shreyas Srinivas]

I think what you are missing is a Value or NormalForm type

[Shreyas Srinivas]

In this case a predicate would suffice

[Paige Thomas]

I'm sorry, I'm not sure I entirely follow. Are we saying that this definition of big step reduction is wrong, or just the statement of the theorem, or both?

[Paige Thomas]

Shreyas Srinivas said:

In this case a predicate would suffice

Like one of these?

mutual
def is_normal_form :
  Expr_ → Prop
  | Expr_.Var _ => True
  | Expr_.App a n => is_neutral_normal_form a ∧ is_normal_form n
  | Expr_.Lam _ n => is_normal_form n

def is_neutral_normal_form :
  Expr_ → Prop
  | Expr_.Var _ => True
  | Expr_.App a n => is_neutral_normal_form a ∧ is_normal_form n
  | _ => False
end


mutual
def is_weak_normal_form :
  Expr_ → Prop
  | Expr_.Var _ => True
  | Expr_.App a n => is_neutral_weak_normal_form a ∧ is_weak_normal_form n
  | Expr_.Lam _ _ => True

def is_neutral_weak_normal_form :
  Expr_ → Prop
  | Expr_.Var _ => True
  | Expr_.App a n => is_neutral_weak_normal_form a ∧ is_weak_normal_form n
  | _ => False
end


mutual
def is_head_normal_form :
  Expr_ → Prop
  | Expr_.Var _ => True
  | Expr_.App a _ => is_neutral_head_normal_form a
  | Expr_.Lam _ n => is_head_normal_form n

def is_neutral_head_normal_form :
  Expr_ → Prop
  | Expr_.Var _ => True
  | Expr_.App a _ => is_neutral_head_normal_form a
  | _ => False
end


mutual
def is_weak_head_normal_form :
  Expr_ → Prop
  | Expr_.Var _ => True
  | Expr_.App a _ => is_neutral_weak_head_normal_form a
  | Expr_.Lam _ _ => True

def is_neutral_weak_head_normal_form :
  Expr_ → Prop
  | Expr_.Var _ => True
  | Expr_.App a _ => is_neutral_weak_head_normal_form a
  | _ => False
end

I'm not sure if these are defined correctly either.

[Paige Thomas]

I have proofs of

example
  (sub : Symbol_ → Expr_ → Expr_ → Expr_)
  (M N : Expr_)
  (h1 : is_bn_big_step sub M N) :
  is_weak_head_normal_form N :=

and

example
  (sub : Symbol_ → Expr_ → Expr_ → Expr_)
  (M N : Expr_)
  (h1 : is_bn_big_step sub M N) :
  Relation.ReflTransGen (is_bn_small_step sub) M N :=

[Shreyas Srinivas]

I will respond in a few hours, but basically it doesn't have to be that complicated. The value language or normal form language needs to be merely a subtype of the expression language

[Shreyas Srinivas]

About the definition of big step semantics. Definitions are the writer's choice, so I wouldn't call them wrong. They're just inconvenient in this case. Having said that, big step semantics is usually taught as a way to side-step all the unwanted challenges of handling reduction rules such as getting into nonterminating reduction sequences. So it usually takes the form $expr \downarrow value$

[Shreyas Srinivas]

Of course in a formalization $value$ is often an $expr$ constructed in a certain way. But the valueness of the reduction target is enforced by a predicate

[Paige Thomas]

I'm trying to learn the lambda calculus by formalizing it as I go, and I was trying to prove the theorem above as a way to check that I had the definitions right. Maybe the question I should ask is, what would the standard definitions for small step and big step semantics for call by name, call by value, applicative order, and normal order look like in Lean, for instance if they were in Mathlib, and the definition of lambda terms used strings for the type of variables as above.

[Paige Thomas]

(instead of say de Bruijn indexes, or locally nameless, or something else)

[Paige Thomas]

I'm kind of surprised actually that I don't see the lambda calculus in Mathlib, maybe I should try to make a PR with what I have for definitions, and get feedback on them there?

[Paige Thomas]

Or has someone already started on this?

[Yaël Dillies]

@Sky Wilshaw has had ideas in this direction

[Paige Thomas]

Kayla Thomas said:

I'm kind of surprised actually that I don't see the lambda calculus in Mathlib, maybe I should try to make a PR with what I have for definitions, and get feedback on them there?

I'm sorry, I didn't mean that in any kind of disparaging way.

[Yaël Dillies]

Nono, it did not feel disparaging :smile:

[Kyle Miller]

I've heard that one design problem is that there are lots of variations on lambda calculus, so which one would be "the" calculus? Or, can it be designed to be extensible to support most (all?) variations?

[Paige Thomas]

I'm just learning it, so I'm not sure. If not, maybe different namespaces/files/folders for each variation, and proofs showing equivalence where possible?

[Yaël Dillies]

That's precisely where Sky's ideas help :smiling_face: No lamda calculus can supersede the other (eg the recursors they want to generate are incompatible), so one has to do several proofs of their various properties. However, one can parametrise lambda calculi by the various constructs they accept as primitives and then prove a lot of theorems for all lambda calculi simultaneously by pushing the case splits inside the proofs.

[Sky Wilshaw]

If I remember correctly, the reason why I didn't go ahead with writing a full lambda calculus and PRing to mathlib was because there was no obvious "right" or "most general" formulation - even wrt (e.g.) names of bound variables.

[Sky Wilshaw]

But anyway, here's my general idea: you make a type that parametrises which features you want in your lambda calculus, and then you make your type of terms inductively:

structure LambdaCalculus where
  hasVar : Bool
  hasLambda : Bool
  hasPair : Bool

inductive LambdaTerm (C : LambdaCalculus)
  | var : C.hasVar → ℕ → LambdaTerm C
  | lam : C.hasLambda → LambdaTerm C → LambdaTerm C
  | pair : C.hasPair → LambdaTerm C → LambdaTerm C → LambdaTerm C
  | left : C.hasPair → LambdaTerm C → LambdaTerm C
  | right : C.hasPair → LambdaTerm C → LambdaTerm C
  | ...

[Sky Wilshaw]

Kyle Miller said:

Or, can it be designed to be extensible to support most (all?) variations?

As I understand it, the general difficulty is unifying the different perspectives on naming. I wonder if an implementation in terms of nominal sets could subsume both approaches.

[Sky Wilshaw]

(The approaches being explicit names vs de Bruijn indices, etc.)

[Sky Wilshaw]

Of course, this approach (like the others I've seen) has the other difficulty that it's fundamentally non-extensible. Typeclasses can only help so much when all of your proofs are structural induction. I don't know a good fix.

[Paige Thomas]

Is it an issue with things not working in Mathlib, or just redundant work, to have more than one variation?

[Sky Wilshaw]

Mostly redundant work as I see it - but mathlib likes having the "most general version" of a thing, and this idea seems incompatible with that viewpoint so far.

[Sky Wilshaw]

The true "most general version" would be a typed lambda calculus, where the UTLC is encoded by setting all of the types to be the same.

[Sky Wilshaw]

Or even further, just all of the calculus of constructions... The point is that it's not clear where to stop! (At least to me.)

[Kyle Miller]

So for untyped lambda calculus, reflexive objects it is! :laughing:

[Paige Thomas]

Maybe a standalone project outside of mathlib? I'd like to use it as a learning aid, so I would be aiming for less generalization.

[Sky Wilshaw]

Yes, this is very doable as a standalone project.

[Shreyas Srinivas]

To answer your original question @Kayla Thomas : here is a good example of how to formalise this: https://gitlab.mpi-sws.org/FP/semantics-2023/-/blob/main/theories/type_systems/stlc/lang.v?ref_type=heads

[Shreyas Srinivas]

It is in Coq, and follows a specific call by value convention for evaluation. In the exercises you find call by name as well

[Paige Thomas]

Awesome, thank you!

[Shreyas Srinivas]

Yaël Dillies said:

That's precisely where Sky's ideas help :smiling_face: No lamda calculus can supersede the other (eg the recursors they want to generate are incompatible), so one has to do several proofs of their various properties. However, one can parametrise lambda calculi by the various constructs they accept as primitives and then prove a lot of theorems for all lambda calculi simultaneously by pushing the case splits inside the proofs.

I had a similar idea for algorithms formalisation. A inductive type for imperative combinators, parametrised by a type of queries.

[Shreyas Srinivas]

The queries can be any basic operations you use, from subsets of the plain RAM model to complex query models

[Shreyas Srinivas]

The complexity claim would be parametrised by the query type and simply count how many times each query is called.

[Shreyas Srinivas]

Then prove a number of meta theorems about complexity on this combinator language

[Shreyas Srinivas]

The call by name version is here: https://gitlab.mpi-sws.org/FP/semantics-2023/-/blob/main/theories/type_systems/stlc/exercises01_sol.v?ref_type=heads

[Paige Thomas]

Thank you!

[Shreyas Srinivas]

Also, I translated these files and proofs to lean last year and was able to get shorter proofs in many cases using tacticals

[Paige Thomas]

Nice. Is the translation in a public repo?

[Shreyas Srinivas]

No. I wrote them as ports of my assignments and iirc we weren't supposed to make those public

[Shreyas Srinivas]

Now ofc the solutions are available

[Shreyas Srinivas]

I'd have to dig around. It'll take me less time to recreate one of these files than find it

[Paige Thomas]

Oh. Are you saying it is ok to make them public now though?

[Shreyas Srinivas]

No I never uploaded the lean versions

[Shreyas Srinivas]

It's buried somewhere deep in one of my machines

[Paige Thomas]

No problem.

[Shreyas Srinivas]

Hopefully not in windows. I haven't updated it in months

[Paige Thomas]

:)

[Patrick Stevens]

My spidey senses are tingling a bit at this hasPair : Bool idea. Doesn't that make it hard to phrase "here is how I added pairs to my lambda calculus that previously lacked them" - e.g. doesn't "lambda plus var" give you access to an implementation of "pair" through the Church encoding? Or is that considered out of scope?

[Shreyas Srinivas]

Church encodings are painful to deal with. Some syntax sugar can make life simple

[Shreyas Srinivas]

As I guessed it didn't take too long to convert a reasonable chunk of that Coq code to lean. I skipped contextual semantics although that's one of the best ways to formulate this stuff I have seen. I have set up sorried out theorem statements that compare big-step and small-step semantics

Code clue

import Mathlib

namespace STLC

inductive Binder where
  | Named (name : String)
  | Anon
deriving DecidableEq

inductive Expr where
  | Var (x : String)
  | Lam (x : Binder) (e : Expr)
  | App (e₁ e₂ : Expr)
  | LitInt (n : Int)
  | Plus (e₁ e₂ : Expr)

inductive Val where
  | LitInt (n : Int)
  | Lam (x : Binder) (e : Expr)

def ofVal (v : Val) : Expr :=
  match v with
  | .LitInt n => .LitInt n
  | .Lam x e => .Lam x e

def toVal (e : Expr) : Option Val :=
  match e with
  | .LitInt n =>  some <| .LitInt n
  | .Lam x e => some <| .Lam x e
  | _ => none

def isVal (e : Expr) : Prop :=
  match e with
  | .LitInt _
  | .Lam _ _ => True
  | _ => False

lemma to_of_val : toVal (ofVal v) = some v := by
  cases v <;> rfl

lemma of_to_val : toVal e = some v → ofVal v = e := by
  intro h
  cases e
    <;> cases v
    <;> simp_all [toVal, ofVal]

lemma is_val_of_val : isVal (ofVal v) := by
  cases v <;> simp [isVal, ofVal]
-- Op Sem
-- Substitution function

def subst (x : String) (esub e : Expr) : Expr :=
  match e with
  | .LitInt n => .LitInt n
  | .Var y =>
        if x = y then esub else .Var y
  | .Lam y e =>
        .Lam y <| if y = .Named x then e else subst x esub e
  | .App e₁ e₂ => .App (subst x esub e₁) (subst x esub e₂)
  | .Plus e₁ e₂ => .Plus (subst x esub e₁) (subst x esub e₂)
-- substitution function for binders
def substBinder (b : Binder) (esub : Expr) : Expr → Expr :=
  fun e =>
    match b with
    | .Named x => subst x esub e
    | .Anon => e
-- small step semantics. Deterministic right to left call-by-value
inductive Step : Expr → Expr → Prop where
  | StepBeta :
      isVal e' →
      Step (.App (.Lam x e) e') (substBinder x e' e)
  | StepAppL :
      isVal e₂ →
      Step e₁ e₁' →
      Step (.App e₁ e₂) (.App e₁' e₂)
  | StepAppR :
      Step e₂ e₂' →
      Step (.App e₁ e₂) (.App e₁ e₂')
  | StepPlusRed :
      Step (.Plus (.LitInt n₁) (.LitInt n₂)) (.LitInt (n₁ + n₂))
  | StepPlusL :
      isVal e₂ →
      Step e₁ e₁' →
      Step (.Plus e₁ e₂) (.Plus e₁' e₂)
  | StepPlusR :
      Step e₂ e₂' →
      Step (.Plus e₁ e₂) (.Plus e₁ e₂')

inductive RTCStep : Expr → Expr → Prop where
  | Base : RTCStep e e
  | Inductive : Step e₁ e₂ → RTCStep e₂ e₃ → RTCStep e₁ e₃


abbrev reducible (e : Expr) :=
  ∃ e', Step e e'
-- Big Step Semantics
inductive BigStep : Expr → Val → Prop where
| Lit : BigStep (.LitInt n) (.LitInt n)
| Lam : BigStep (.Lam x e) (.Lam x e)
| Add :
    BigStep e₁ (.LitInt v₁) →
    BigStep e₂ (.LitInt v₂) →
    BigStep (.Plus e₁ e₂) (.LitInt (v₁ + v₂))
| App :
    BigStep e₁ (.Lam x e) →
    BigStep e₂ v₂ →
    BigStep (substBinder x (ofVal v₂) e) v →
    BigStep (.App e₁ e₂) v

@[simp]
lemma big_step_vals : BigStep (ofVal v) v := by
  cases v <;> constructor

lemma big_step_inv_vals : BigStep (ofVal v) w → v = w := by
  intro H
  simp [ofVal] at H -- The coq proof didn't need this
  cases v <;> cases H <;> rfl


lemma StepRTC_for_BigStep : BigStep e v → RTCStep e (ofVal v) := by
  intro BigH
  cases v <;> simp_all [ofVal]  <;>
    cases BigH <;> try apply RTCStep.Base
  case LitInt.Add => sorry
  case LitInt.App => sorry
  case Lam.App => sorry

lemma BigStep_for_StepRTC_val : RTCStep e e' → isVal e' → ∃ v, some v = toVal e' ∧ BigStep e v := by
  sorry

end STLC

Note : I am using a lot of autoImplicits here

[Sky Wilshaw]

Patrick Stevens said:

My spidey senses are tingling a bit at this hasPair : Bool idea. Doesn't that make it hard to phrase "here is how I added pairs to my lambda calculus that previously lacked them" - e.g. doesn't "lambda plus var" give you access to an implementation of "pair" through the Church encoding? Or is that considered out of scope?

I only added pairs as an example to show how to add other language features - there are plenty of other things you could add that would maybe be more useful.

[Paige Thomas]

Thank you!

[Paige Thomas]

Hmm. Now I'm confused as to where the definitions of the big step semantics in my reference come from and how they relate to what is given in this code (if they do).

[Shreyas Srinivas]

The reference looks like a more theoretical paper.

[Asei Inoue]

this is my attempt to formalize program semantics

https://github.com/Seasawher/ConcreteSemantics.lean