Skip to content

Instantly share code, notes, and snippets.

@andrcmdr

andrcmdr/λcube.md

Forked from brendanzab/λcube.md
Last active February 21, 2025 12:28
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save andrcmdr/7121c3d9eb83f06785d8055a5c3604a3 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save andrcmdr/7121c3d9eb83f06785d8055a5c3604a3 to your computer and use it in GitHub Desktop.
Download ZIP
Lambda λ Cube (by Hendrik 'Henk' Pieter Barendregt)
Raw
λcube.md

System λ

The untyped lambda calculus

e ::=             terms:
  x               variable
  e e             application
  λ x . e         abstraction

System λ→

The simply Typed Lambda Calculus)

  • Terms depending on terms
t ::=             types:
  a               variable
  t → t           arrow type

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction

System λΠ

  • Terms depending on terms
  • Types depending on terms
t ::=             types:
  a               variable
  t → t           arrow type
  Π x : t . e     abstraction

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction

System λ2 (System F)

  • Terms depending on terms
  • Terms depending on types
k :: =            kinds:
  *               type of types

t ::=             types:
  a               variable
  t → t           arrow type

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction
  e t             type application
  Λ a : k . e     type abstraction

System λω_ (System Fω_)

  • Terms depending on terms
  • Types depending on types
k :: =            kinds:
  *               type of types
  k → k           arrow kind

t ::=             types:
  a               variable
  t → t           arrow type
  t t             application
  ∀ a : k . t     universal quantification

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction

System λω (System Fω)

λ2 + λω_

  • Terms depending on terms
  • Terms depending on types
  • Types depending on types
k :: =            kinds:
  *               type of types
  k → k           arrow kind

t ::=             types:
  a               variable
  t → t           arrow type
  t t             application
  ∀ a : k . t     universal quantification

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction
  e t             type application
  Λ a : k . e     type abstraction

System λΠω (Calculus of Constructions)

  • Terms depending on terms
  • Terms depending on types
  • Types depending on types
  • Types depending on terms
e ::=
  x              variables
  *              type of types
  e e            application
  ∀ x : e . e    quantification (∀ and Π)
  λ x : e . e    abstraction (λ and Λ)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment