3
$\begingroup$

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.

$\endgroup$
3
  • 2
    $\begingroup$ 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. $\endgroup$ Feb 6, 2013 at 15:38
  • $\begingroup$ @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. $\endgroup$
    – Guy Coder
    Feb 6, 2013 at 15:43
  • $\begingroup$ @DaveClarke Can you make your comment an answer so I can accept it and others can see this question has an accepted answer. Thanks. $\endgroup$
    – Guy Coder
    Jan 26, 2020 at 12:11

1 Answer 1

0
$\begingroup$

Since I have waited years for Dave Clarke to answer I am just going to copy his comment so that others can see this has an answer.

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 σ and v refer to. Many many papers studying programming language constructs will introduce their own λ-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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.