Simply Typed Lambda Calculus in mathlib

Stream: general

[zbatt]

I noticed recently there's no formalization for simply typed lambda calculus in the mathlib. I'm a fairly inexperienced Lean user, but I do have a formalization that I did for a project here. I would be really interested in trying to get this to a place where it could live in the mathlib. There are a bunch of auxillary lemmas, but the main "theorem-worthy" results I have right now are proofs of Unicity of typing, Progress, and Preservation. (There are also a couple of results I proved only because they were asked as a homework question in one of my classes - lines 300 to 565 are probably not worth putting in the mathlib) Besides concerns of style which obviously needs to be improved, I have a couple of questions:

1. Is this even a reasonable foundation for STLC in Lean? If not, why not and how can I improve it?

2. Is this a thing that belongs in the mathlib?

3. If the answers to the previous two questions were yes, how would I decide the "canonical" version of STLC to work with. What types should I include? How should substituion be defined? etc.

Thank you so much and I would be eager for any feedback about my code or otherwise!

[Johan Commelin]

I'm not an expert on lambda calculus at all. But I think such things could definitely go in mathlib.

[Kevin Buzzard]

Does this development need anything at all of the current theory in mathlib?

[zbatt]

Kevin Buzzard said:

Does this development need anything at all of the current theory in mathlib?

Sorry, what do you mean by this?

[Johan Commelin]

Are you depending on parts of mathlib?

[Johan Commelin]

It looks like you depend on some tactics, and maybe a few things about option?

[zbatt]

Ah ok, yes that's exactly right. I use some of the mathlib tactics such as induction' and split_ifs. I'm realizing now that the option import was from an earlier version and I no longer need it so mathlib dependencies are limited to just tactics.

[Yuyang Zhao]

I've heard another definition from others, which translates into lean is something like the following (there are some missed things), but I'm not sure it's better.

import tactic.basic

/-! # Simply typed λ-calculus -/

universes u

namespace lambda_calculus

structure simply_typed : Type (u+1) :=
(base_types : set (Type u))

namespace simply_typed

inductive type (L : simply_typed)
| base_type {T} (hT : T ∈ L.base_types) : type
| fun_type : type → type → type
export type

localized "infixr (name := fun_type) ` ⥤ `:10 := lambda_calculus.simply_typed.type.fun_type"
  in lambda_calculus.simply_typed

variables (L : simply_typed.{u})

abbreviation context := list L.type

variable {L}

def context.cons (Γ : L.context) (α : L.type) : L.context := α :: Γ

localized "infixl (name := context.cons) ` ◂ `:75 := lambda_calculus.simply_typed.context.cons"
  in lambda_calculus.simply_typed

inductive var : L.context → L.type → Type (u + 1)
| z {Γ α}   :            var (Γ ◂ α) α
| s {Γ α β} : var Γ α → var (Γ ◂ β) α

def v0 {L : simply_typed} {Γ α} : var (Γ ◂ α) α := @var.z L Γ α

inductive term : L.context → L.type → Type (u + 1)
| var {Γ α}   : var Γ α                     → term Γ α
| abs {Γ α β} : term (Γ ◂ α) β              → term Γ (α ⥤ β)
| app {Γ α β} : term Γ (α ⥤ β) → term Γ α → term Γ β

localized "prefix (name := term.var) `#`:1500 := lambda_calculus.simply_typed.term.var"
  in lambda_calculus.simply_typed
localized "prefix (name := term.abs) `ƛ `:10 := lambda_calculus.simply_typed.term.abs"
  in lambda_calculus.simply_typed
localized "infixl (name := term.app) ` · `:1000 := lambda_calculus.simply_typed.term.app"
  in lambda_calculus.simply_typed

variables {Γ : L.context} {α β γ : L.type}

namespace combinator
def I : term Γ (α ⥤ α) := ƛ #v0
def K : term Γ (α ⥤ β ⥤ α) := ƛ (ƛ #v0.s)
def L : term Γ ((α ⥤ β ⥤ γ) ⥤ (α ⥤ β) ⥤ α ⥤ γ) := ƛ ƛ ƛ (#v0.s.s · #v0) · (#v0.s · #v0)
end combinator

end simply_typed

end lambda_calculus

[Johan Commelin]

@zbatt I should maybe walk back my statement a bit. As I said I'm not an expert on lambda calculus at all. It is my opinion that some type theoretic stuff should be welcome in mathlib. But for the particular details, I would rather defer to someone more knowledgeable.

[Floris van Doorn]

I think a formalization of lambda calculus / type theory suffers from a similar problem as that of graph theory: there are many different (non-equivalent) formulations, and it depends on your goals which formulation you want to use.
A difference with graph theory is that eventually quite some mathematical results will use graphs, but I think the usage of a formalization of (simply) typed lambda calculus will be quite limited.

Some choices you have to make when formalizing type theory. Of course there is the question of simply typed lambda calculus vs dependent type theory, but even in simply typed lambda calculus, there are many questions:

• What are your base types?
• How do you encode variables (named, de Bruijn variables, locally nameless, ...)?
• Do lambda abstractions come with their type?
• Do you want to define well-typed terms in terms of raw terms, or do you want to directly define the "well-typed terms in context Γ with type A" directly as an inductive definition?

My preference is to wait with including type theory/lambda calculus in mathlib, until someone does a relatively big formalization and shows that their formalization is actually usable, or maybe until multiple (groups of) people want to work on it independently...

Btw, @zbatt: one thing in your formalization that is not very standard is that you allow for infinite contexts.

[Alex J. Best]

@Floris van Doorn what about putting it in achive instead?

[Floris van Doorn]

If the code quality is good, I'm fine with that.

[Floris van Doorn]

Although that might send the wrong message that lambda calculus does not belong to mathlib, which is not the message I want to send...

[zbatt]

Floris van Doorn said:

I think a formalization of lambda calculus / type theory suffers from a similar problem as that of graph theory: there are many different (non-equivalent) formulations, and it depends on your goals which formulation you want to use.
A difference with graph theory is that eventually quite some mathematical results will use graphs, but I think the usage of a formalization of (simply) typed lambda calculus will be quite limited.

You have to make many choices when formalizing type theory. Of course there is the question of simply typed lambda calculus vs dependent type theory, but even in simply typed lambda calculus, there are many questions:

• What are your base types?
• How do you encode variables (named, de Bruijn variables, locally nameless, ...)?
• Do lambda abstractions come with their type?
• Do you want to define well-typed terms in terms of raw terms, or do you want to directly define the "well-typed terms in context Γ with type A" directly as an inductive definition?

My preference is to wait with including type theory/lambda calculus in mathlib, until someone does a relatively big formalization and shows that their formalization is actually usable, or maybe until multiple (groups of) people want to work on it independently...

Btw, zbatt: one thing in your formalization that is not very standard is that you allow for infinite contexts.

That makes a lot of sense. I definitely am not the person that should be making those decisions about the canonical formalization of this. I was hoping that maybe there was some standard I was unaware of which is part of the reason I posted this, but if not, those decisions should absolutely be made by someone with more experience.

And thanks for the note about infinite contexts! I'll be sure to get around to updating that.

[Thorsten Altenkirch]

In general I think it is a bad idea to define untyped terms first. I would always do it intrinsically, see attached. stl.lean

[Thorsten Altenkirch]

This certainly works very well in agda using dependently typed pattern matching, I don't know how well this fits into Lean.
However, I would argue that this is conceptually the right definition, since there is no reason to define untyped terms if you are interested in typed ones. We have also done this for dependent types, e.g. see https://dl.acm.org/doi/abs/10.1145/2837614.2837638