### Transcription

Computational lambda-calculus and monadsEugenio Moggi LFCSDept. of Comp. Sci.University of EdinburghEH9 3JZ Edinburgh, [email protected] 1988AbstractThe λ-calculus is considered an useful mathematical tool in the studyof programming languages, since programs can be identified with λ-terms.However, if one goes further and uses βη-conversion to prove equivalenceof programs, then a gross simplification 1 is introduced, that may jeopardisethe applicability of theoretical results to real situations. In this paper weintroduce a new calculus based on a categorical semantics for computations.This calculus provides a correct basis for proving equivalence of programs,independent from any specific computational model.1IntroductionThis paper is about logics for reasoning about programs, in particular for provingequivalence of programs. Following a consolidated tradition in theoretical computerscience we identify programs with the closed λ-terms, possibly containing extraconstants, corresponding to some features of the programming language under consideration. There are three approaches to proving equivalence of programs: The operational approach starts from an operational semantics, e.g. a partial function mapping every program (i.e. closed term) to its resulting value (ifany), which induces a congruence relation on open terms called operationalequivalence (see e.g. [Plo75]). Then the problem is to prove that two termsare operationally equivalent.On leave from Università di Pisa. Research partially supported by the Joint CollaborationContract # ST2J-0374-C(EDB) of the EEC 1programs are identified with total functions from values to values1

The denotational approach gives an interpretation of the (programming) language in a mathematical structure, the intended model. Then the problemis to prove that two terms denote the same object in the intended model. The logical approach gives a class of possible models for the (programming)language. Then the problem is to prove that two terms denotes the same objectin all possible models.The operational and denotational approaches give only a theory (the operationalequivalence and the set T h of formulas valid in the intended model respectively),and they (especially the operational approach) deal with programming languageson a rather case-by-case basis.On the other hand, the logical approach gives a logical consequence relation (Ax A iff the formula A is true in all models of the set of formulas Ax), whichcan deal with different programming languages (e.g. functional, imperative, nondeterministic) in a rather uniform way, by simply changing the set of axioms Ax,and possibly extending the language with new constants. Moreover, the relation is often semidecidable, so it is possible to give a sound and complete formal systemfor it, while T h and are semidecidable only in oversimplified cases.We do not take as a starting point for proving equivalence of programs thetheory of βη-conversion, which identifies the denotation of a program (procedure)of type A B with a total function from A to B, since this identification wipes outcompletely behaviours like non-termination, non-determinism or side-effects, thatcan be exhibited by real programs. Instead, we proceed as follows:1. We take category theory as a general theory of functions and develop on top acategorical semantics of computations based on monads (this is my maincontribution).2. We show that w.l.o.g. one may consider only monads over a topos (because ofcertain properties of the Yoneda embedding), and therefore one can use higherorder intuitionistic logic.3. We investigate how datatypes, in particular products, relates to computations(previous work by category-theorists is particularly useful here).At the end we get a formal system, the computational lambda-calculus (λc -calculusfor short), similar to P P λ (see [GMW79]) for proving equivalence and existenceof programs, which is sound and complete w.r.t. the categorical semantics of computations. The methodology outlined above is inspired by [Sco80]2 , in particular theview that “category theory comes, logically, before the λ-calculus”led us to considera categorical semantics of computations first, rather than trying to hack directly onthe rules of βη-conversion to get a correct calculus.2“I am trying to find out where λ-calculus should come from, and the fact that the notion ofa cartesian closed category is a late developing one (Eilenberg & Kelly (1966)), is not relevant tothe argument: I shall try to explain in my own words in the next section why we should look to itfirst”.2

1.1Related workThe operational approach to find correct λ-calculi w.r.t. an operational equivalence,was first considered in [Plo75] for call-by-value and call-by-name operational equivalence. This approach was later extended, following a similar methodology, to consider other features of computations like nondeterminism (see [Sha84]) and sideeffects (see [FFKD86, MT89]).The calculi based only on operational considerations, like the λv -calculus, aresound and complete w.r.t. the operational semantics, i.e. a program M has a valueaccording to the operational semantics iff it is provably equivalent to a value (notnecessarily the same) in the calculus, but they are too weak for proving equivalencesof programs.The denotational approach may suggest important principles, e.g. fix-point induction (see [Sco93, GMW79]), that can be found only after developing a semanticsbased on mathematical structures rather than term models, but it does not giveclear criteria to single out the general principles among the properties satisfied bythe model.The approach adopted in this paper generalises the one followed in [Ros86,Mog86] to obtain the λp -calculus, i.e. the calculus for reasoning about partial computations (or equivalently, about partial functions). In fact, the λp -calculus (likethe λ-calculus) amounts to a particular λc -theory.A type theoretic approach to partial functions and computations is attempted in[CS87, CS88] by introducing a new type constructor Ā, whose intuitive meaning isthe set of computations of type A. However, Constable and Smith do not adequatelycapture the general axioms for (partial) computations as we (and [Ros86]) do, sincethey lack a general notion of model and rely only on domain- and recursion-theoreticintuition.2A categorical semantics of computationsThe basic idea behind the semantics of programs described below is that a programdenotes a morphism from A (the object of values of type A) to T B (the object ofcomputations of type B). There are many possible choices for T B correspondingto different notions of computations, for instance in the category of sets the setof partial computations (of type B) is the lifting B { } and the set of nondeterministic computations is the powerset P(B). Rather than focus on specificnotions of computations, we will try to identify the general properties that theobject T B of computations must have.Definition 2.1A computational model is a monad (T, η, µ) over a category C, i.e. a functor3

.T : C C and two natural transformations η: IdC T and µ: T 2 T s.t.T 3AµT AT µA T 2A T 2A T 2A @@ id@ TA@@RµAµAηT ATA TAT ηAµATAidT A TAwhich satisfies also an extra equalizing requirement: ηA : A T A is an equalizerof ηT A and T (ηA ), i.e. for any f : B T A s.t. f ; ηT A f ; T (ηA ) there exists aunique m: B A s.t. f m; ηA 3 .Remark 2.2 Intuitively ηA : A T A gives the inclusion of values into computations,while µA : T 2 A T A flatten a computation of a computation into a computation.However, it is the equalizing requirement which ensures that ηA is a (strong)mono rather than an arbitrary morphism.According to the view of “programs as functions from values to computations” thenatural category for interpreting programs is not C, but the Kleisli category.Definition 2.3 (see [Mac71])Given a monad (T, η, µ) over C, the Kleisli category CT , is the category s.t. : the objects of CT are those of C the set CT (A, B) of morphisms from A to B in CT is C(A, T B)ηA the identity on A in CT is A TA the composition of f CT (A, B) and g CT (B, C) in CT isfTgµCA T B T 2C TCRemark 2.4 Our view of programs corresponds to call-by-value parameter passing,but there is an alternative view of “programs as functions from computations tocomputations” corresponding to call-by-name (see [Plo75] and Section 5). In anycase, the fundamental issue is that there is a subset of the computations, the values,which has special properties and should not be forgotten. By taking call-by-valuewe can stress better the importance of values. Moreover, call-by-name can be moreeasily represented in call-by-value than the other way around.Before going into the details of the interpretation we consider some examples ofcomputational models over the category of sets.Example 2.5 non-deterministic computations:3The other property for being an equalizer, namely ηA ; ηT A ηA ; T (ηA ), follows from thenaturality of η4

T ( ) is the covariant powerset functor, i.e.T (A) P(A) and T (f )(X) is the image of X along f ηA is the singleton map a 7 {a} µA is the big union map X 7 XIt is easy to check the equalizing requirement, in factηT A : X 7 {X}T (ηA ): X 7 {{x} x X}therefore ηT A (X) T (ηA )(X) iff X is a singleton.Example 2.6 computations with side-effects: T ( ) is the functor (S ( S)), where S is a nonempty set of stores.Intuitively a computation takes a store and returns a value together with themodified store. ηA is the map a 7 (λs: S.ha, si) µA is the map f 7 (λs: S.eval(f s)), i.e. µA (f ) is the computation that givena store s, first computes the pair computation-store hf 0 , s0 i f s and thenreturns the pair value-store ha, s00 i f 0 s0 .One can verify for himself that other notions of computation (e.g. partial, probabilistic or non-deterministic with side-effects) fit in this general definition.2.1A simple language and its interpretationThe aim of this section is to focus on the crucial ideas of the interpretation, and thelanguage has been oversimplified (for instance terms have exactly one free variable)in order to define its interpretation in any computational model without requiringany additional structure on it. However, richer languages, e.g. with product andfunctional types, will be considered in Section 3. The term language we introduceis parametric in a signature (i.e. a set of base types and unary function symbols),therefore its interpretation in a computational model (T, η, µ) over a category C, isparametric in an interpretation of the symbols in the signature. Given an interpretation [[A]] for any base type A, i.e. an object of the Kleislicategory CT , then the interpretation of a type τ : : A T τ is an object [[τ ]]of CT defined in the obvious way, namely [[T τ ]] T [[τ ]]. Given an interpretation [[f ]] for any unary function symbol f of arity τ1 τ2 ,i.e. a morphism from [[τ1 ]] to [[τ2 ]] in CT , then the interpretation of a well-formedterm x: τ e: τ 0 is a morphism [[x: τ e: τ 0 ]] from [[τ ]] to [[τ 0 ]] in CT defined byinduction on the derivation of x: τ e: τ 0 (see Table 1). On top of the term language we consider two atomic predicates: equivalenceand existence (see Table 2).5

RULE SYNTAXvarx: τ x: τSEMANTICS η[[τ ]]letx: τ e1 : τ1 g1x1 : τ 1 e 2 : τ 2 g2x: τ (let x1 e1 in e2 ): τ2 g1 ; T g2 ; µ[[τ2 ]]i.e. g1 ; g2 in the Kleisli categoryf : τ1 τ2x: τ e1 : τ1x: τ f (e1 ): τ2 g1 g1 ; T [[f ]]; µ[[τ2 ]]x: τ e: τ 0x: τ [e]: T τ 0 g g; ηT [[τ 0 ]]x: τ e: T τ 0x: τ µ(e): τ 0 g g; µ[[τ 0 ]][]µTable 1: Terms and their interpretationRULE SYNTAXeqx: τ1 e1 : τ2 x: τ1 e2 : τ2 x: τ1 e1 e2 : τ2 SEMANTICSg1g2g 1 g2exx: τ1 e: τ2x: τ1 e τ2 g g factors through η[[τ2 ]]i.e. there exists (unique) h s.t. g h; η[[τ2 ]]Table 2: Atomic assertions and their interpretation6

Remark 2.7 The let-constructor is very important semantically, since it correspondsto composition in the Kleisli category CT . While substitution (of a variable with anexpression denoting a value) corresponds to composition in C.In the λ-calculus (let x e in e0 ) is usually treated as syntactic sugar for (λx.e0 )e,and this can be done also in the λc -calculus (because of (β) in Table 8). However, wethink that this is not the right way to proceed, because it amounts to understandingthe let-constructor, which makes sense in any computational model, in terms ofconstructors that make sense only in λc -models. On the other hand, (let x e in e0 )cannot be reduced to the more basic substitution (i.e. e0 [x: e]) without collapsingCT to C.Remark 2.8 The existence of e does not simply means that the computation denotedby e terminates (as, say, in the logic of partial terms), but something stronger,namely that e denotes a value. For instance: a non-deterministic computation exists iff it gives exactly one result; a computation with side-effects exists iff it does not change the store.According to the paradigm of Categorical Logic, formulas should be interpreted bysubobjects. This can be achieved by interpreting the binary predicate : τ , i.e.equality of computations of type τ , by the diagonal T [[τ ]] and the unary predicate τ , i.e. existence of computations of type τ , by η[[τ ]] , which is a mono because ofthe equalizing requirement.2.2Embedding of a computational model in a toposWe show that any computational model (T, η, µ) over a small category C can be liftedto a computational model (T̂ , η̂, µ̂) over the topos Cˆ of presheaves (i.e. the functoropcategory SetC ), and that such a lifting commutes with the Yoneda embedding Yˆ i.e.of C into C,T̂ (Y ) Y(T ) ,η̂Y Y(η ) ,µ̂Y Y(µ )As pointed out in [Sco80] such an embedding enable us to switch from the equational (and rather inexpressive) calculus of an arbitrary computational model to theintuitionistic higher-order logic of (a computational model over) a topos.The monad (T̂ , η̂, µ̂) is defined by using the Yoneda embedding Y: C Cˆ andˆLanY , i.e. the left adjoint to Y; : CˆC CˆC mapping any F : C Cˆ to its left Kanextension4 along Y (see [Mac71]), namely:T̂ Lan(T ; Y) ,η̂ Lan(η; Y) ,µ̂ Lan(µ; Y)The commutativity with the Yoneda embedding (stated above) and the fact that Yinduces a full and faithful embedding Y of CT into CˆT̂ follow from some well-knownproperties of Y and LanY , summarised in the following lemma:ˆLemma 2.9 If C is small category, then Y: C Cˆ and LanY : CˆC CˆC are full andˆfaithful. Moreover Y; LanY F F for every F : C C.4the left adjoint LanY exists because Set is small cocomplete7

3Extending the languageIn this section we discuss how to interpret terms with any finite number of variables(instead of exactly one as in Table 1) and how datatypes relate to computations. Wewill consider only product and functional types, because sum types are completelystraightforward5 . This will allow a comparison with cartesian closed categories (ccc)and partial cartesian closed categories (pccc).The standard requirement on a category for interpreting terms with any finitenumber of variables is that it must have finite products, so that the interpretation [[f ]]of a function symbol f of arity τ τ is a morphism from [[ (τ )]] (i.e. [[τ1 ]] . . . [[τn ]])to [[τ ]] and similarly the interpretation of a well-formed term x1 : τ1 , . . . , xn : τn e: τis a morphism from [[ (τ )]] to [[τ ]].According to the view of “programs as functions from values to computations”,products should be taken in C, since a value of type A B is a pair of values one oftype A and the other of type B, even though the natural category for interpretingprograms is CT . However, products are not enough to extend the interpretation toterms with more than one free variable, because we must be able to take a pairvalue-computation or computation-computation and turn it into a computation ofa pair.Example 3.1 Let g2 : τ1 T τ2 and and g: τ1 τ2 T τ be the interpretations ofx1 : τ1 e2 : τ2 and x1 : τ1 , x2 : τ2 e: τ respectivelly. The problem with terms havingmore than one free variable (and its solution) becomes apparent if we try to interpretx1 : τ1 (let x2 e2 in e): τ , when both x1 and x2 are free in e.If T were IdC , then [[x1 : τ1 (let x2 e2 in e): τ ]] would be hidτ1 , g2 i; g. In thegeneral case, Table 1 says that ; above is indeed composition in the Kleisli category,therefore hidτ1 , g2 i; g becomes hidτ1 , g2 i; T g; µτ . But in hidτ1 , g2 i; T g; µτ there is atype mismatch, since the codomain of hidτ1 , g2 i is τ1 T τ2 , while the domain ofT g is T (τ1 τ2 ). To get around this we require T to have a tensorial strengthtA,B : A T B T (A B) (see below), so that x1 : τ1 (let x2 e2 in e): τ will beinterpreted by hidτ1 , g2 i; tτ1 ,τ2 ; T g; µτ .Similarly for interpreting x: τ f (e1 , e2 ): τ 0 , we need a natural transformationψA,B : (T A T B) T (A B) (see Definition 3.4), which given a pair of programsreturns a program computing a pair. More precisely, let gi : τ T τi be the interpretation of x: τ ei : τi , then [[x: τ f (e1 , e2 ): τ 0 ]] is hg1 , g2 i; ψτ1 ,τ2 ; T [[f ]]; µ.Definition 3.2 Let C be a category with finite products, and rA , αA,B,C and cA,B bethe natural isomorphisms:r(1 A) A,α(A B) C A (B C),c(A B) (B A)A computational cartesian model over C is a computational model (T, η, µ) overC together with a tensorial strength tA,B : (A T B) T (A B) of T , i.e. a natural5coproducts are preserved by the inclusion of C into the Kleisli category CT8

transformation s.t.1 TAt1,A T (1 A)@@ r@ [email protected]@tA B,C(A B) T CT rA TA T ((A B) C)αA,B,T CT αA,B,C idA tB,CtA,B CA (B T C) A T (B C) T (A (B C))satisfying the following diagrams:A BidA BidA ηB A TB ηA BtA,BidA µBA T 2B A B T (A B) µA BtA,T BT tA,B 2 T (A T B) T (A B)Remark 3.3 In general the tensorial strength t has to be given as an extra parameterfor models. However, t is uniquely determined (but it may not exists) by T andthe cartesian structure on C, when C has enough points, i.e. if f, g: A B, thenf g ( h: 1 A.h; f h; g).The diagrams above are not new, they are all in [Koc70b], where a one-one correspondence is established between functorial and tensorial strengths 6 : the first two diagrams, saying that t is a tensorial strength of T , are (1.7) and(1.8) in [Koc70b]. By Theorem 1.3 in [Koc70b] t induces a functorial strengthof T making T a C-enriched (also called strong) functor. the last two diagrams say that η and µ are natural transformations between.suitable C-enriched functors, namely η: IdC T and µ: T 2 T (see Remark 1.5 in [Koc70b]).6If V is a monoidal closed category, then a functorial strength of an endofunctor T on Vis a natural transformation stA,B : B A T B T A making T a V -enriched functor. Intuitively stinternalizes the action of T on morphisms.9

Definition 3.4 The tensorial strength t induces a monoidal structure, i.e. anatural transformation ψA,B : (T A T B) T (A B) and a map ψ1 : 1 T 1ψA,B cT A,T B ; tT B,A ; T (cT B,A ; tA,B ); µA B,ψ1 η 1satisfying certain diagrams (see [EK66]).The morphism ψA,B : (T A T B) T (A B) has the correct domain and codomainto interpret the pairing of a computation of type A with one of type B (obtainedby first evaluating the first argument and then the second), while the morphismψ1 interprets the computation of hi (the empty tuple). There is also a dual notionof pairing, namely ψ̃A,B cA,B ; ψB,A ; T cB,A , which amounts to first evaluating thesecond argument and then the first (see (2.1) and (2.2) at page 14 in [Koc70b]).The categorical interpretation of functional types in a computational model resembles that of partial function spaces in a pccc (see [Ros86, Mog86]):Definition 3.5 Let C be a category with finite products. A λc -model over C is acomputational cartesian model (T, η, µ, t) over C together with a family of universalarrows evalTA,B : (BTA A) T B (in C) s.t. for any f : (C A) T B there exists aunique h: C BTA (denoted by ΛTA,B,C (f )) making the following diagram commuteBTAevalTA,B A TB h idAfC AA more suggestive way of saying the same thing is that there is a natural isomorphismCT (C A, B) C(C, BTA ), where A, B and C vary over C op , CT and C respectively.The simple language introduced in Section 2.1 and its interpretation can beextended according to the additional structure available in a cartesian computationalmodel (T, η, µ, t) on a category C with finite products: there is a new type 1, interpreted by the terminal object of C, and a new typeconstructor τ1 τ2 interpreted by the product of [[τ1 ]] and [[τ2 ]] in C the interpretation of a well-formed term Γ e: τ , where Γ is a sequencex1 : τ1 , . . . , xn : τn , is a morphism from [[Γ]] (i.e. [[τ1 ]] . . . [[τn ]]) to [[τ ]] in CT(see Table 3)7 .In a λc -model the interpretation can be extended to functional types and λ-terms,1 ]]namely: the type τ1 * τ2 is interpreted by [[τ2 ]][[τT , while abstraction and applicationare interpreted as in Table 4.7We do not have to consider nonunary functions explicitly, because in a language with productsthey can be treated as unary functions from a product type.10

RULE SYNTAXSEMANTICSvarx1 : τ1 , . . . , xn : τn xi : τi πin ; η[[τi ]]letΓ e 1 : τ1Γ, x1 : τ1 e2 : τ2Γ (let x1 e1 in e2 ): τ2 g1 g2 hid[[Γ]] , g1 i; t[[Γ]],[[τ1]] ; T g2 ; µ[[τ2 ]]Γ : 1 ![[Γ]] ; η1 where !A is the only morphism from A to 1hiΓ e 1 : τ1Γ e 2 : τ2Γ he1 , e2 i: τ1 τ2 g1 g2 hg1 , g2 i; ψ[[τ1 ]],[[τ2 ]]Γ e: τ1 τ2Γ πi (e): τ1 g g; T (πi )πiTable 3: Terms and their interpretationRULE SYNTAXSEMANTICSλΓ, x1 : τ1 e2 : τ2 gΓ (λx1 : τ1 .e2 ): τ1 * τ2 ΛT[[τ1 ]],[[τ2 ]],[[Γ]](g); η[[τ1 *τ2 ]]appΓ e 1 : τ1Γ e: τ1 * τ2Γ e(e1 ): τ2 g1 g hg, g1 i; app[[τ1 ]],[[τ2 ]]where appA,B : T (BTA ) T A T B is ψBTA ,A ; T (evalTA,B ); µBTable 4: λ-terms and their interpretation11

3.1ExamplesIn this section we show few general ways of constructing computational models fromsimpler ones. Each of them amounts to adding a new feature to computations.Example 3.6 Let (T, η, µ, t) be a cartesian computational model on a topos (forsimplicity Set), then the following are cartesian computational models: Let S be inhabited (i.e. 1 S), then the model (TS , η S , µS , tS ) of T -computationswith side-effects in S isTS ( ) ( S)STηAS ΛTS,(A S),A (ηA S )µSA ΛTS,(A S),(T 2 A) (evalTS,(TS A S) ; T (evalTS,(A S) ); µA S )S 1tSA,B ΛTS,(A S),(A TS B) (αA,TS B,S ; (idA evalTS,(B S) ); tA,B S ; T (αA,B,S)) the model (TE , η E , µE , tE ) of T -computations with exceptions in E isTE ( ) T ( E)ηAE in1 ; ηA EµEA T ([idT (A E) , in2 ; ηA E ]); µA EtEA,B tA,B E ; T (dA,B,E ; [idA B , π2 ])ininwhere A 1 A B 2 B is a coproduct diagram,[f, g]: A B C is the mediating morphism of f : A C and g: B C, i.e.the unique h: A B C s.t. f in1 ; h and g in2 ; h,ddA,B,C is the natural isomorphism A (B C) (A B) (A C) expressingcommutativity of coproducts w.r.t. products8These constructions provide basic building blocks, that can be combined togetherfor instance: TE S ( ) T (( S) E)S and TS E ( ) T (( E) S)S combine side-effectsand exceptions. In the former the store is lost, when an exception is raised,while in the latter it is retained.( ) If T is the monad of R-continuations9 , i.e. T ( ) RR , then the monadA STS (A) RS (R ) combines continuation and side-effects as done when givingthe denotational semantics of imperative languages with goto.Monad-morphisms provide a simple tool for relating two computational models:Definition 3.7Given two cartesian computational models (T, η T , µT , tT ) and (S, η S , µS , tS ) over the8which holds in cartesian closed categories, but not in general9It is not clear what properties R must have in order for the monad T to satisfy the equalizingrequirement. Intuitively one expects that the category C must have enough R-observations, i.e.f g ( h: B R.f ; h g; h) for any f, g: A B12

same category, a monad-morphism from the first to the second model is a natural.transformation σ: T S s.t. :ηATAidA TA µTAηAS TA T AσA2σA A2µSA T 2AtTA,B T (A B)A TBA σB A SBσA B S(A B)tSA,Bwhere σ 2 is the horizontal composition, i.e. σA2 T (σA ); σSA σT A ; S(σA ).Example 3.8 For each of the computational model constructions defined above thereis a monad morphism from T to it, namely:. σ S : T TS is the natural transformation s.t. σAS is ΛTS,A S,T (A) (tA,S ). σ E : T TE is the natural transformation s.t. σAE is T (inA,E1 )Monad-morphisms are not adequate for relating λc -models, because the naturaltransformation σ cannot be extended to functional types. Instead, one can usea notion of logical relation between λc -models (see [Mog88] for various notions oflogical relation between λp -models).4The λc-calculusIn this section we present a formal system, the λc -calculus, based on many sortedintuitionistic logic with two atomic predicates, existence and equivalence.We claim that the formal system is sound and complete w.r.t. λc -models (overtoposes). Soundness amounts to showing that the inference rules are admissible inany λc -model, while completeness amounts to showing that any λc -theory has aninitial model (given by a term-model construction).The inference rules of the λc -calculus are for deriving sequents Γ. A, where Γis a sequence of type assignments x: τ , is a set of formulas and A is a formula s.t.the free variables FV( , A) of and A are included in the declared variables DV(Γ)of Γ. The intuitive meaning of Γ. A is: “for all variables in Γ, if all formulas in are true, then A is true”. We have intentionally left the set of formulas unspecified,since it depends on what class of models one is interested in. There is a minimaland maximal choice for the set of formulas: if the language has to be interpreted in any λc -model, then only atomic formulas (including e e0 : τ and e τ ) are allowed if the language has to be interpreted only in λc -model over a topos, then allhigher order formulas are allowed.13

The inference rules are partitioned as follows: general rules for (higher order) intuitionistic logic, where variables range overvalues, while terms denotes computations (see Table 5 for the most relevantrules)10 the basic inference rules for computational models (see Table 6) the inference rules for product types (see Table 7) the inference rules for functional types (see Table 8)Remark 4.1 A comparison among λc -, λv - and λp -calculus shows that: the λv -calculus proves less equivalences between λ-terms, e.g. (λx.x)(yz) (yz) is provable in the λc - but not in the λv -calculus the λp -calculus proves more equivalences between λ-terms, e.g. (λx.yz)(yz) (yz) is provable in the λp - but not in the λc -calculus, because y can be aprocedure, which modifies the store (e.g. by increasing the value contained ina local static variable) each time it is executed. a λ-term e has a value in the λc -calculus, i.e. e is provably equivalent to somevalue (either a variable or a λ-abstraction), iff e has a value in the λv -calculus(λp -calculus)5Untyped λc-modelsIt is well-known that a categorical model for the untyped λ-calculus is a reflexiveobject D D D in a cartesian closed category (see [Sco80, Bar82]). In a λc -modelthere are two analogs for a reflexive object: VTV N (see [Ong88] V and NTT N for similar definitions in the context of partial cartesian closed categories).In the first case we have a model of call-by-value. In fact the elements of Vcorrespond to functions from values to computations (as VTV stands for V T V ), andtherefore an element can be applied to a computation e only after e has been evaluated . In the second case we have a model of call-by-name, since the elements of Ncorrespond to functions from computations to computations.The call-by-value and call-by-name interpretations are defined by induction onthe derivation of the untyped λ-term x1 , . . . , xn e (with let): Let G: VTV V be an isomorphism with inverse F , then the call-by-valueinterpretation of x1 , . . . , xn e is a morphism from V n to T V (see Table 9),because free variables range over values.10The general rules of sequent calculus (in [Sza69]), more precisely those for substitution andquantifiers, have to be modified slightly, because variables range over values. These modificationsare similar to those introduced in the logic of partial terms (see Section 2.4 in [Mog88]).14

We write [x: e] for the substitution of x with e in .E.xsubstΓ. x τΓ. e τΓ, x: τ. AΓ. A[x: e] is an equivalence relationcongrΓ. e1 e2 : τΓ. A[x: e1 ]Γ. A[x: e2 ]Table 5: General rulesWe write (let x e in e) for (let x1 e1 in (. . . (let xn en in e) . . .)), where n is the lenghtof the sequence x (and e). In particular, (let in e) stands for e.idcomplet.ξlet.βlet.fE.[ ]Γ. (let x e in x) e: τΓ. (let x2 (let x1 e1 in e2 ) in e) (let x1 e1 in (let x2 e2 in e)): τΓ. e1 e01 : τΓ, x: τ. e2 e02 : τ 0Γ. (let x e1 in e2 ) (let x e01 in e02 ): τ 0Γ. (let x1 x2 in e) e[x1 : x2 ]: τΓ. f (e) (let x e in f (x)): τΓ. [e] T τΓ. e e0 : τT.ξΓ. [e] [e0 ]: T τlet.µT.βT.ηΓ. µ(e) (let x e in µ(x)): τΓ. µ([e]) e: τΓ. [µ(x)] x: T τΓ. e τ and Γ. [e] (let x e in [x]): τ are interderivableTable 6: rules for let and computational types15x1 6 FV(e)

E. 1.ηE.h ilet.h iE.πilet.πi .β .ηΓ. 1Γ. x: 1Γ. hx1 , x2 i τ1 τ2Γ. he1 , e2 i (let x1 , x2 e1 , e2 in hx1 , x2 i): τ1 τ2Γ. πi (x) τiΓ. πi (e1 , e2 ) (let x1 , x2 e1 , e2 in πi (x1 , x2 )): τiΓ. πi (hx1 , x2 i) xi : τiΓ. hπ1 (x), π2 (x)i x: τ1 τ

Computational lambda-calculus and monads Eugenio Moggi LFCS Dept. of Comp. Sci. University of Edinburgh EH9 3JZ Edinburgh, UK [email protected] October 1988 Abstract The -calculus is considered an useful mathematical tool in the study of programmin