# λ-Calculus extensions: meaning of extension symbols

When working with λ-Calculus I see lots of extensions that use other symbols such as ∀ <:Top {} ←, which are from "Types and Programming Languages" (WorldCat) by Benjamin C. Pierce.

Name                   Extends/Based on Figure                          Figure                                                   Page
B unyped                                                                3-1 Booleans (B)                                         34
B ℕ (untyped)          Extends 3-1 B                                    3-2 Arithmetic expressions (ℕB)                          41
→ (untyped)                                                             5-3 Unyped lambda-calculus (λ)                           72
B (typed)              Extends 3-1 B                                    8-1 Typing rules for booleans (B)                        93
B ℕ (typed)            Extends 3-1, 8-1 B                               8-2 Typing rules for numbers (ℕB)                        93
→ (typed)              Based on5-3 λ                                    9-1 Pure simply typed lambda-calculus (λ→)               103
→ Unit                 Extends 9-1 λ→                                   11-2 Unit type                                           119
→ as                   Extends 9-1 λ→                                   11-3 Ascription                                          122
→ let                  Extends 9-1 λ→                                   11-4 let binding                                         124
→ x                    Extends 9-1 λ→                                   11-5 Pairs                                               126
→ {}                   Extends 9-1 λ→                                   11-6 Tuples                                              128
→ {}                   Extends 9-1 λ→                                   11-7 Records                                             129
→ {} let p (untyped)   Extends 11-7, 11-4                               11-8 (Untyped) record patterns                           131
→ +                    Extends 9-1 λ→                                   11-9 Sums                                                132
→ +                    Extends 9-1 λ→                                   11-10 Sums (with unique typing)                          135
→ <>                   Extends 9-1 λ→                                   11-11 Variants                                           136
→ fix                  Extends 9-1 λ→                                   11-12 General recursion                                  144
→ B List               Extends 9-1 λ→ with 8-1 booleans                 11-13 Lists                                              147
→ Unit Ref             Extends 9-1 λ→ with 11-2 Unit                    13-1 References                                          166
→ error                Extends 9-1 λ→                                   14-1 Errors                                              172
→ error try            Extends 9-1 λ→ with 14-1 Errors                  14-2 Error handling                                      174
→ exceptions           Extends 9-1 λ→                                   14-3 Exceptions carrying values                          175
→ <: Top               Extends 9-1 λ→                                   15-1 Simply typed lambda-calculus with subtyping (λ<:)   186
→ {} <:                Extends 15-1 λ<: and 11-7 Records                15-3 Records and subtyping                               187
→ <: Bot               Extends 15-1 λ<:                                 15-4 Bottom type                                         192
→ <> <:                Extends 15-1 λ<: and 11-11 Simple variant rules  15-5 Variants and subtyping                              197
→ {} <:                Extends 15-1 λ<: and 15-3 Records and subtyping  16-1 Subtype relataion with records (compact version)    211
→ {} <:                                                                 16-2 Algorithmic subtyping                               212
→ {} <:                                                                 16-3 Algorithmic typing                                  217
→ u                    Extends 9-1 λ→                                   20-1 Iso-recursive types (λu)                            276
→∀                     Based on 9-1 λ→                                  23-1 Polymorphic lambda-calculus (System F)              343
→∀∃                    Extends 23-1 System F                            24-1 Exestential types                                   366
→∀∃ Top                Based on 23-1 System F and 15-1 simple subtyping 26-1 Bounded quantification (kernel F<:)                 392
→∀∃ Top full           Extends 26-1 F<:                                 26-2 "Full" bounded quantification                       395
→∀<: Top ∃             Extends 26-1 F<: and 24-1 unbounded existentials 26-3 Bounded existential quantification (kernel variant) 406
→∀<: Top                                                                28-1 Exposure Algorithm for F<:                          418
→∀<: Top               Extends 16-3 λ<:                                 28-2 Algorithmic typing for F<:                          419
→∀<: Top               Extends 16-2 λ<:                                 28-3 Algorithmic subtyping for kernel F<:                422
→∀<: Top full          Extends 28-3                                     28-4 Algorithmic subtyping for full F<:                  424
-⇒                     Extends 9-1 λ→                                   29-1 Type operators and kinding (λω)                     466
-∀⇒                    Extends 29-1 λω and 23-1 System F                30-1 Higher-order polymorphic lambda-calculus (Fω)       450
-∀∃⇒                   Extends 30-1 Fω and 24-1                         30-2 Higher-order existential types                      452
-∀⇒<: Top              Based on 30-1 Fω and 16-1 kernel F<:             31-1 Higher-order bounded quantification (Fω<:)          470
-∀<: Top {}←           Based on 26-1 F<: with 11-7 records              32-1 Polymorphic update                                  485


or use of σ and ν as in

"From λσ to λν-a Journey through Calculi of Explicit Substitutions" by Pierre Lescanne.

and of course Barendregt's Lambda Cube

Note: For the Weak systems ω should be underlined.

λ→   The Simply Typed Lambda Calculus
λω   Weak Lambda Omega
λ2   Polymorphic or Second Order, Typed Lambda Calculus
λω   The System Fω
λP   LF
λPω  Weak Lambda P omega
λP2  Lambda P2
λPω  The Calculus of Constructions


Is there any standard or commonality to the use of these symbols? Where can I find a listing of their meaning.

Also, as I have shown with the extenstions using TAPL, is there any list of the most noteworthy calculi with there symbols, defnition and what they extend?

I am really after a DAG of related λ-Calculi that gives a brief explaination of each one.

• If I am not mistaken, you have just given such a list. And if you read the abstract of the paper you just linked, then you'll find what $\sigma$ and $v$ refer to. Many many papers studying programming language constructs will introduce their own $\lambda$-variant, so the only way of knowing what each one is is by consulting the research papers. Pierce's book goes a long way, though, with the standard ones. Feb 6, 2013 at 15:38
• @DaveClarke I suspected "introduce their own λ-variant". As you are more of an authority on this than me, again you have saved me many days of searching. If after a few days no one comes up with a better answer then post it as an answer and I will accept it. Feb 6, 2013 at 15:43
• @DaveClarke Can you make your comment an answer so I can accept it and others can see this question has an accepted answer. Thanks. Jan 26, 2020 at 12:11