WIXLIB

LambdaCalculusas The Internal Language of Cartesian ClosedCategoriesJacob Neumann80-413/713 - November 2020

0 CCCs: An Algebraic Perspective

Terminal ObjectsA terminal object is an object 1, such that for every object A of C,there is a morphism !A : A 1A!A1such thatfor all f : A 1,0Lambda Calculusf !ACCCs: An Algebraic Perspective

ProductsFor each A, B, their product is an object A B with an operationh , i : Hom(Z, A) Hom(Z, B) Hom(Z, A B)and maps p1 : A B A and p2 : A B B such that, for all f, g, h,p1 hf, gi fp2 hf, gi ghp1 h, p2 hi h0Lambda CalculusCCCs: An Algebraic Perspective

ExponentialsFor all B, C, their exponential is an object C B equipped with anoperationcurry : Hom(A B, C) Hom(A, C B )and a map : C B B C such that for all u : A B C and allv : A CB, ((curry u) 1B ) ucurry( (v 1B )) vRecall v 1B : A B C B B is hv p1 , p2 i.0Lambda CalculusCCCs: An Algebraic Perspective

CBcurry uACB B(curry u) 1B CuA BNote: the operation v 7 (v 1B ) is a kind of “uncurrying”.0Lambda CalculusCCCs: An Algebraic Perspective

Adjunction DefinitionThis definition is equivalent to the definition of exponentials as rightadjoints:( ) B a ( )B .The required isomorphism is given bycurry : Hom(A B, C) Hom(A, C B )uncurry : Hom(A, C B ) Hom(A B, C)where uncurry(v) hv p1 , p2 i (v 1B ).0Lambda CalculusCCCs: An Algebraic Perspective

is the counit of the adjunction.Recall that every adjunction L a R gives rise to a counit naturaltransform : L R 1dom(R)In the case of ( ) B a ( )B , this means C : C B B Cnatural in C. This is the “evaluation” morphism for C B .0Lambda CalculusCCCs: An Algebraic Perspective

SummaryHere, A, B, C, Z range over all objects of CStructureRequired DataLawsTerminalObject!A : A 1For all k : A 1, k !ABinaryProductsp1 : A B Ap2 : A B Bh , i : Hom(Z, A) Hom(Z, B) Hom(Z, A B)For all f : Z A, g : Z B,p1 hf, gi fp2 hf, gi gFor all h : Z A B,h hp1 h, p2 hi C : C B B Ccurry : Hom(A B, C) Hom(A, C B )For all u : A B C, v : A C B , ((curry u) 1B ) ucurry( (v 1B )) vExponentials0Lambda Calculus

1 The Simply-Typed Lambda Calculus

History & Motivation of the Lambda CalculusThe lambda calculus Developed in 1930s by Alonzo Church as a mathematical model ofcomputation (prior to the existence of electronic computers).Provably equivalent to other such notions (e.g. Turing machines) Has “untyped” and “typed” variants Theoretical basis of functional programming and type theory1Lambda CalculusThe Simply-Typed Lambda Calculus

Lambda AbstractionLambda Calculus studies functions between types, which can be thoughtof like sets. We denote “x is an element of T ” as x : T instead of x T .To define a function from T1 to T2 , it suffices to specify a rule assigningto each x : T1 some expression e : T2 , where the value of e, in general,can depend on x.(λx.e) : T1 T2This is the function which “accepts” x : T1 and “returns” e : T2 .1Lambda CalculusThe Simply-Typed Lambda Calculus

General Setup We’ll build up a system of types T We’ll define contexts, which consist of several “typed variabledeclarations” In a context Γ, we’ll form terms of given types In a context Γ, we’ll prove equalities between terms1Lambda CalculusThe Simply-Typed Lambda Calculus

TypesTo get started, we fix some set Ty0 of basic types, and recursivelygenerate the set of all types Ty from it.T, T 0 :: 1Lambda CalculusT01T T0T T0(T0 Ty0 )(Unit type)(Product types)(Arrow types)The Simply-Typed Lambda Calculus

ContextsFor some variable name x and some T Ty, we can form the typejudgment x : T , read “x is of type T ”.A context Γ is a finite list of typing judgments x1 : T1 , . . . , xn : Tn ,Γ :: Γ, x : T(Empty context)(Context Extension)(We usually make some syntactic requirements on contexts, e.g. that all the variable names are distinct)1Lambda CalculusThe Simply-Typed Lambda Calculus

General SetupX We’ll build up a system of types TX We’ll define contexts, which consist of several “typed variabledeclarations” In a context Γ, we’ll form terms of given types In a context Γ, we’ll prove equalities between terms1Lambda CalculusThe Simply-Typed Lambda Calculus

Term-Building ActivitiesNow recursively build up terms-in-context of these types. We writeΓ t:Tto indicate that t is a term of type T in context Γ. We may also have some basic terms t0 Tm0 , each of a specifiedbasic type. If t0 Tm0 and is specified to be of type T0 , thenΓ t0 : T 0for any Γ ? is always a term of type 1:Γ ?:11Lambda Calculusfor any ΓThe Simply-Typed Lambda Calculus

Term-Building If Γ t1 : T1 and Γ t2 : T2 ,Γ (t1 , t2 ) : T1 T2 If Γ p : T1 T2 ,Γ fst(p) : T1andΓ snd(p) : T2 If Γ, x : T1 e : T2 ,Γ (λx.e) : T1 T2 If Γ f : T1 T2 and Γ v : T1 ,Γ (f v) : T21Lambda CalculusThe Simply-Typed Lambda Calculus

Rules of Lambda CalculusΓ, x : T x : T(Var.)Γ x2 : T2(Weak.)Γ, x1 : T1 x2 : T2Γ t:TΓ t t1Lambda CalculusΓ t1 t2Γ t2 t1Γ t1 t2 Γ t2 t3Γ t1 t3The Simply-Typed Lambda Calculus

Unit & Product RulesΓ w:1Γ w ?Γ p : T1 T2Γ (fst(p), snd(p)) pΓ t1 : T1Γ t2 : T 2Γ t1 : T 1Γ t2 : T 2Γ fst(t1 , t2 ) t1Γ snd(t1 , t2 ) t21Lambda CalculusThe Simply-Typed Lambda Calculus

Beta & EtaΓ (λx.e) : T1 T2Γ v : T1(β)Γ (λx.e)(v) e[v/x]Γ f : T1 T2(η)Γ (λx.f x) f1Lambda CalculusThe Simply-Typed Lambda Calculus

ExampleClaim 1 For any types T1 , T2 , T3 and any context Γ, there exist terms incontext ΓΓ split : (T1 T2 T3 ) (T1 T2 ) (T1 T3 )Γ pair : (T1 T2 ) (T1 T3 ) (T1 T2 T3 )such thatΓ, f : T1 T2 T3 pair(split(f )) fΓ, g1 : T1 T2 , g2 : T1 T3 split(pair(g1 , g2 )) (g1 , g2 )1Lambda CalculusThe Simply-Typed Lambda Calculus

Proof (sketch)split : λf.(λx.fst(f x), λx.snd(f x))pair : λp.λx.(fst(p)(x), snd(p)(x))1Lambda CalculusThe Simply-Typed Lambda Calculus

2 Categorical Semantics

High-level ideaThe preceding syntactic structure of types T , contexts Γ, andterms-in-context Γ x : T is the language of lambda calculus, L.“Interpret” L inside a cartesian closed category C, i.e. we want somemapping1J K : L CIn particular, JT K and JΓK will be objects of C, and JΓ x : T K will be amorphism JΓK JT K. Goal:Γ t1 t2 is provable12 JΓ t1 K JΓ t2 KJ K is actually a functor, if we view L as a category in an appropriate way.Lambda CalculusCategorical Semantics

Interpreting TypesT, T 0 :: (T0 Ty0 )(Unit type)(Product types)(Arrow types)T01T T0T T0Define the interpretation of types, J K : Ty Ob(C). We must supply JT0 K Ob(C) for each T0 Ty0 J1K 1, the terminal object JT1 T2 K JT1 K JT2 K JT1 T2 K JT2 KJT1 K2Lambda CalculusCategorical Semantics

Interpreting ContextsRecall that Ctx, the set of all contexts, is defined recursively byΓ :: Γ, x : T(Empty context)(Context Extension)So define J K : Ctx Ob(C) Interpret the empty context as 1, the terminal object JΓ, x : T K JΓK JT K2Lambda CalculusCategorical Semantics

Interpreting TermsTo complete our interpretation of the lambda calculus, we must interpretterms-in-context as morphisms of C. Specifically,JΓ t : T K : JΓK JT K. If t0 Tm0 is a basic term of type T0 , we must pickJ t0 : T0 K : 1 JT0 K For any Γ, JΓ ? : 1K !JΓK .JΓK2Lambda CalculusJΓ ?:1KJ1K 1Γ w:1Γ w ?Categorical Semantics

Structural RulesVariable Rule:Weakening:Γ, x : T x : TΓ x2 : T2Γ, x1 : T1 x2 : T2JΓK JT K2Lambda Calculusp2JT KJΓK JT1 KJΓ x2 :T2 K !JT1 KCategorical SemanticsJT2 K 1 JT2 K

Product TermsJΓ t1 :T1 KJT1 Kp1JΓKJΓ (t1 ,t2 ):T1 T2 KJT1 T2 Kp2JΓ t2 :T2 KJT2 K JΓ (t1 , t2 ) : T1 T2 K hJΓ t1 : T1 K, JΓ t2 : T2 Ki JΓ fst(p) : T1 K p1 JΓ p : T1 T2 K2Lambda CalculusCategorical Semantics

Product RulesΓ p : T1 T2Γ (fst(p), snd(p)) pΓ t1 : T1Γ t2 : T 2Γ fst(t1 , t2 ) t12Lambda CalculusΓ t1 : T 1Γ t2 : T 2Γ snd(t1 , t2 ) t2Categorical Semantics

Arrows are Exponentials Abstraction: want to fulfillΓ, x : T1 e : T2Γ (λx.e) : T1 T2i.e. given JΓK JT1 K JT2 K, define a morphism JΓK JT2 KJT1 K Application: want to fulfillΓ f : T1 T2Γ v : T1Γ (f v) : T2i.e. given JΓK JT2 KJT1 K and JΓK JT1 K, define a morphismJΓK JT2 K2Lambda CalculusCategorical Semantics

λ-AbstractionJT2 KJT1 KJΓ (λx.e):T1 T2 KJΓKJT2 KJT1 K JT1 KJΓ (λx.e):T1 T2 K 1JT1 K JT2 KJΓ,x:T1 e:T2 KJΓ, x : T1 KJΓ (λx.e) : T1 T2 K : curry JΓ, x : T1 e : T2 K2Lambda CalculusCategorical Semantics

ApplicationJΓ f :T1 T2 KJΓKhJΓ f K,JΓ vKiJT2 KJT1 Kp1JT2 KJT1 K JT1 Kp2JΓ v:T1 K JT2 KJT1 KJΓ (f v) : T2 K : hJΓ f : T1 T2 K, JΓ v : T1 Ki2Lambda CalculusCategorical Semantics

BetaIf we define substitution in the appropriate way, the β ruleΓ (λx.e) : T1 T2Γ v : T1(β)Γ (λx.e)(v) e[v/x]is valid for every interpretation of lambda calculus in any CCC, i.e.JΓ (λx.e)(v)K JΓ e[v/x]K. This usually involves proving a“substitution lemma”.2Lambda CalculusCategorical Semantics

EtaThe η ruleΓ f : T1 T2(η)Γ (λx.f x) fis valid for all interpretations: JΓ λx.f xK JΓ f K.This is provedusing the universal property of exponentials.2Lambda CalculusCategorical Semantics

3 Results

SoundnessThm. 1 (Soundness) For any CCC C and any interpretationJ K : L C and any terms t1 , t2 : T in context Γ, if we can deduceΓ t1 t2using the rules of lambda calculus, thenJΓ t1 : T K JΓ t2 : T K.Proof by induction on the deduction of Γ t1 t2 .3Lambda CalculusResults

Isomorphism CorollaryCor. 1.1 If T1 and T2 are types and in any context Γ there exists termsΓ F : T1 T2Γ G : T2 T1such thatΓ, x : T1 G(F (x)) xΓ, y : T2 F (G(y)) ythenJT1 K JT2 K.3Lambda CalculusResults

ApplicationCor 1.2 If C is a CCC, J K : L C, then for any types T1 , T2 , T3 ,(JT2 K JT3 K)JT1 K JT2 KJT1 K JT3 KJT1 KProof : By Claim 1 and Cor 1.1 .3Lambda CalculusResults

Language of a CCCFor any CCC C, we can define the language of C, L(C), to be thelambda calculus language whose basic types are the objects of C whose basic terms of type X are the morphisms 1 X in C.Define a canonical J K : L(C) C by interpreting each basic type andterm as itself.Thm. 2 For any objects X, Y, Z of a cartesian closed category, there isan isomorphism(Y Z)X Y X ZX3Lambda CalculusResults

Further Directions Completeness: Prove that any equality which is valid in every CCC isprovable in the lambda calculus. Duality: Show that the syntax of lambda calculus is – in a sense –dual to its model theory Add fancier stuff:IIIIInitial objectCoproductsNatural numbers object, and other inductive typesDependent types and higher inductive types Do an analogous development for other formal systems and classes ofcategories (categorical logic!)3Lambda CalculusResults

Thank you!3Lambda CalculusResults

The lambda calculus Developed in 1930s by Alonzo Church as a mathematical model of computation (prior to the existence of electronic computers). Provably equivalent to other such notions (e.g. Turing machines) Has \untyped" and \typed" variants Theoretical basis of functional programming and type theory 1 Lambda Calculus The Simply-Typed Lambda .