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.
