In 1936 the notion of intuitive computability was operationalized in two different ways: via Turing machines and via λ-calculus. The difference consisted in manipulating beads (bits) for the former approach versus manipulating trees (rewriting λ-terms) for the latter. Both proposals turned out to formalize the same notion of computability, and led to the Church-Turing Thesis, claiming that intuitive computability is captured in the correct way. This resulted in the foundation of imperative and functional programming. Variants of λ-calculus are being used in another powerful field of applications, namely proof-checking, the basis for certifying mathematical theorems and thereby high tech industrial products. These two areas of research are still being actively investigated and make λ-calculus a major tool in the present stages of science and of the industrial revolution. In this book λ-calculus is considered from another angle: as a study of these tree-like structures, investigating the relation between their shape and their action. This is like studying numbers qualitatively, rather than for their applications dealing quantitatively with objects and phenomena in the world. Barendregt's book `The Lambda Calculus, its Syntax and Semantics' (1981/84), does treat the subject from the same methodological viewpoint, and includes several open conjectures. In the more than four decades that have passed, most - but not all - of these conjectures have been solved, sometimes in ingenious PhD theses. This `Satellite' to the aforementioned book presents these solutions in a uniform style and adds other topics of interest.
Relational models of λ-calculus can be presented as type systems, the relational interpretation of a λ-term being given by the set of its typings. Within a distributors-induced bicategorical semantics generalising the relational one, we identify the class of 'categorified' graph models and show that they can be presented as type systems as well. We prove that all the models living in this class satisfy an Approximation Theorem stating that the interpretation of a program corresponds to the filtered colimit of the denotations of its approximants. As in the relational case, the quantitative nature of our models allows to prove this property via a simple induction, rather than using impredicative techniques. Unlike relational models, our 2-dimensional graph models are also proof-relevant in the sense that the interpretation of a λ-term does not contain only its typings, but the whole type derivations. The additional information carried by a type derivation permits to reconstruct an approximant having the same type in the same environment. From this, we obtain the characterisation of the theory induced by the categorified graph models as a simple corollary of the Approximation Theorem: two λ-terms have an isomorphic interpretation exactly when their Böhm trees coincide.
Turing machines and register machines have been used for decades in theoretical computer science as abstract models of computation. Also the λ-calculus has played a central role in this domain as it allows to focus on the notion of computation itself, while abstracting away from implementation details. The present article starts from the observation that the equivalence between these formalisms is based on the Church-Turing Thesis rather than an actual encoding of λ-terms into Turing (or register) machines. The reason is that these machines are not well-suited for modelling λ-calculus programs. We introduce a new class of abstract machines that we call addressing machines because they are only able to manipulate memory addresses of other machines. The operations performed by a machines are very elementary: load an address in a register, apply a machine to another one via their addresses and, finally, call the address of another machine. We endow addressing machines with an operational semantics based on head-reduction and study their behaviour. The set of addresses of these machines can be easily turned into a combinatory algebra. In order to obtain a model of the full untyped λ-calculus, we need to introduce a rule that bares similarities with the ω-rule and the rule ζβ from combinatory logic.
The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott's continuity, Berry's stability or Kahn and Plotkin's sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.
The call-by-value λ-calculus can be endowed with permutation rules, arising from linear logic proof-nets, having the advantage of unblocking some redexes that otherwise get stuck during the reduction. We show that such an extension allows to define a satisfying notion of Böhm(-like) tree and a theory of program approximation in the call-by-value setting. We prove that all lambda terms having the same Böhm tree are observationally equivalent, and characterize those Böhm-like trees arising as actual Böhm trees of lambda terms. We also compare this approach with Ehrhard's theory of program approximation based on the Taylor expansion of lambda terms, translating each lambda term into a possibly infinite set of so-called resource terms. We provide sufficient and necessary conditions for a set of resource terms in order to be the Taylor expansion of a lambda term. Finally, we show that the normal form of the Taylor expansion of a lambda term can be computed by performing a normalized Taylor expansion of its Böhm tree. From this it follows that two lambda terms have the same Böhm tree if and only if the normal forms of their Taylor expansions coincide.
Despite the fact that call-by-value λ-calculus was defined by Plotkin in 1977, we believe that its theory of program approximation is still at the beginning. A problem that is often encountered when studying its operational semantics is that, during the reduction of a λ-term, some redexes remain stuck (waiting for a value). Recently, Carraro and Guerrieri proposed to endow this calculus with permutation rules, naturally arising in the context of linear logic proof-nets, that succeed in unblocking a certain number of such redexes. In the present paper we introduce a new class of models of call-by-value λ-calculus, arising from non-idempotent intersection type systems. Beside satisfying the usual properties as soundness and adequacy, these models validate the permutation rules mentioned above as well as some reductions obtained by contracting suitable λI-redexes. Thanks to these (perhaps unexpected) features, we are able to demonstrate that every model living in this class satisfies an Approximation Theorem with respect to a refined notion of syntactic approximant. While this kind of results often require impredicative techniques like reducibility candidates, the quantitative information carried by type derivations in our system allows us to provide a combinatorial proof.
The main observational equivalences of the untyped λ-calculus have been characterized in terms of extensional equalities between Böhm trees. It is well known that the λ-theory H*, arising by taking as observables the head normal forms, equates two λ-terms whenever their Böhm trees are equal up to countably many possibly infinite eta-expansions. Similarly, two λ-terms are equal in Morris's original observational theory H+, generated by considering as observable the beta-normal forms, whenever their Böhm trees are equal up to countably many finite eta-expansions. The λ-calculus also possesses a strong notion of extensionality called "the ω-rule", which has been the subject of many investigations. It is a longstanding open problem whether the equivalence Bω obtained by closing the theory of Böhm trees under the ω-rule is strictly included in H+, as conjectured by Sallé in the seventies. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture. The proof technique we develop for proving the latter inclusion is general enough to provide as a byproduct a new characterization, based on bounded eta-expansions, of the least extensional equality between Böhmtrees. Together, these results provide a taxonomy of the different degrees of extensionality in the theory of Böhm trees.
The λ-calculus enjoys the property that each λ-term has at least one fixed point, which is due to the existence of a fixed point combinator. It is unknown whether it enjoys the "fixed point property" stating that each λ-term has either one or infinitely many pairwise distinct fixed points. We show that the fixed point property holds when considering possibly open fixed points. The problem of counting fixed points in the closed setting remains open, but we provide sufficient conditions for a λ-term to have either one or infinitely many fixed points. In the main result of this paper we prove that in every sensible λ-theory there exists a λ-term that violates the fixed point property. We then study the open problem concerning the existence of a double fixed point combinator and propose a proof technique that could lead towards a negative solution. We consider interpretations of the λY-calculus into the λ-calculus together with two Reduction Extension Properties, whose validity would entail the non-existence of any double fixed point combinators. We conjecture that both properties hold when typed λY-terms are interpreted by arbitrary fixed point combinators. We prove Reduction Extension Property I for a large class of fixed point combinators. Finally, we prove that the λY-theory generated by the equation characterizing double fixed point combinators is a conservative extension of the λ-calculus.
We study the relational graph models that constitute a natural subclass of relational models of λ-calculus. We prove that among the λ-theories induced by such models there exists a minimal one, and that the corresponding relational graph model is very natural and easy to construct. We then study relational graph models that are fully abstract, in the sense that they capture some observational equivalence between lambda-terms. We focus on the two main observational equivalences in the λ-calculus, the theory H+ generated by taking as observables the β-normal forms, and H* generated by considering as observables the head normal forms. On the one hand we introduce a notion of λ-König model and prove that a relational graph model is fully abstract for H+ if and only if it is extensional and lambda-Köonig. On the other hand we show that the dual notion of hyperimmune model, together with extensionality, captures the full abstraction for H*.
Differential categories were introduced by Blute, Cockett and Seely to axiomatize categorically Ehrhard and Regnier's syntactic differential operator. We present an abstract construction that takes a symmetric monoidal category and yields a differential category, and show how this construction may be applied to categories of games. In one instance, we recover the category previously used to give a fully abstract model of a nondeterministic imperative language. The construction exposes the differential structure already present in this model, and shows how the differential combinator may be encoded in the imperative language. A second instance corresponds to a new differential cartesian category of games. We give a model of a simply-typed resource calculus, Resource PCF, in this category and show that it possesses the finite definability property. Comparison with a semantics based on Bucciarelli, Ehrhard and Manzonetto's relational model reveals that the latter also possesses this property and is fully abstract.
We study the semantics of a resource sensitive extension of the lambda calculus in a canonical reflexive object of a category of sets and relations, a relational version of Scott's original model of the pure lambda calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a "must" parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula. As an intermediate result we prove that the exception mechanism is not essential in the finite sub-calculus.
MLF is a type system extending ML with first-class polymorphism as in system F. The main goal of the present paper is to show that MLF enjoys strong normalization, i.e., it has no infinite reduction paths. The proof of this result is achieved in several steps. We first focus on xMLF, the Church-style version of MLF, and show that it can be translated into a calculus of coercions: terms are mapped into terms and instantiations into coercions. This coercion calculus can be seen as a decorated version of system F, so that the simulation result entails strong normalization of xMLF through the same property of system F. We then transfer the result to all other versions of MLF using the fact that they can be compiled into xMLF and showing there is a bisimulation between the two. We conclude by discussing what results and issues are encountered when using the candidates of reducibility approach to the same problem.
The differential λ-calculus is a paradigmatic functional programming language endowed with a syntactical differentiation operator that allows to apply a program to an argument in a linear way. One of the main features of this language is that it is resource conscious and gives the programmer suitable primitives to handle explicitly the resources used by a program during its execution. The differential operator also allows to write the full Taylor expansion of a program. Through this expansion every program can be decomposed into an infinite sum (representing non-deterministic choice) of 'simpler' programs that are strictly linear. The aim of this paper is to develop an abstract 'model theory' for the untyped differential λ-calculus. In particular, we investigate what should be a general categorical definition of denotational model for this calculus. Starting from the work of Blute, Cockett and Seely on differential categories we provide the notion of Cartesian closed differential category and we prove that linear reflexive objects living in such categories constitute sound models of the untyped differential λ-calculus. We also give sufficient conditions for Cartesian closed differential categories to model the Taylor expansion. This entails that every model living in such categories equates all programs having the same full Taylor expansion. We then provide a concrete example of a Cartesian closed differential category modeling the Taylor expansion, namely the category MRel of sets and relations from finite multisets to sets. We prove that the relational model D of λ-calculus we have recently built in MRel is linear, and therefore it is also a model of the untyped differential λ-calculus. Finally, we study the relationship between the differential λ-calculus and the resource calculus, a functional programming language combining the ideas behind the differential λ-calculus with those behind the lambda-calculus with multiplicities. We define two translation maps between these two calculi and we study the properties of these translations. In particular, from this analysis it follows that the two calculi share the same notion of model. Therefore the resource calculus can be interpreted by translation into every linear reflexive object living in a Cartesian closed differential category.
We recently introduced an extensional model of the pure λ-calculus living in a canonical cartesian closed category of sets and relations. In the present paper, we study the non-deterministic features of this model. Unlike most traditional approaches, our way of interpreting non-determinism does not require any additional powerdomain construction. We show that our model provides a straightforward semantics of non-determinism (may convergence) by means of unions of interpretations, as well as of parallelism (must convergence) by means of a binary, non-idempotent operation available on the model, which is related to the mix rule of Linear Logic. More precisely, we introduce a λ-calculus extended with non-deterministic choice and parallel composition, and we define its operational semantics (based on the may and must intuitions underlying our two additional operations). We describe the interpretation of this calculus in our model and show that this interpretation is 'sensible' with respect to our operational semantics: a term converges if, and only if, it has a non-empty interpretation.
The aim of this article is twofold. From one side we survey the knowledge we have acquired these last ten years about the lattice of all λ-theories (equational extensions of untyped λ-calculus) and the models of lambda calculus via universal algebra. This includes positive or negative answers to several questions raised in these years as well as several independent results, the state of the art about the long-standing open questions concerning the representability of λ-theories as theories of models, and 26 open problems. On the other side, against the common belief, we show that lambda calculus and combinatory logic satisfy interesting algebraic properties. In fact the Stone representation theorem for Boolean algebras can be generalized to combinatory algebras and λ-abstraction algebras. In every combinatory and λ-abstraction algebra, there is a Boolean algebra of central elements (playing the role of idempotent elements in rings). Central elements are used to represent any combinatory and λ-abstraction algebra as a weak Boolean product of directly indecomposable algebras (i.e. algebras that cannot be decomposed as the Cartesian product of two other non-trivial algebras). Central elements are also used to provide applications of the representation theorem to lambda calculus. We show that the indecomposable semantics (i.e. the semantics of lambda calculus given in terms of models of lambda calculus, which are directly indecomposable as combinatory algebras) includes the continuous, stable and strongly stable semantics, and the term models of all semisensible λ-theories. In one of the main results of the article we show that the indecomposable semantics is equationally incomplete, and this incompleteness is as wide as possible.
A longstanding open problem is whether there exists a non-syntactical model of the untyped λ-calculus whose theory is exactly the least λ-theory λβ. In this paper we investigate the more general question of whether the equational/order theory of a model of the untyped λ-calculus can be recursively enumerable (r.e. for brevity). We introduce a notion of effective model of λ-calculus, which covers in particular all the models individually introduced in the literature. We prove that the order theory of an effective model is never r.e.; from this it follows that its equational theory cannot be λβ or λβη. We then show that no effective model living in the stable or strongly stable semantics has an r.e. equational theory. Concerning Scott's semantics, we investigate the class of graph models and prove that no order theory of a graph model can be r.e., and that there exists an effective graph model whose equational/order theory is the minimum among the theories of graph models. Finally, we show that the class of graph models enjoys a kind of downwards Lowenheim-Skolem theorem.
Addressing machines have been introduced as a formalism to construct models of the pure, untyped λ-calculus. We extend the syntax of their programs by adding instructions for executing arithmetic operations on natural numbers, and introduce a reflection principle allowing certain machines to access their own address and perform recursive calls. We prove that the resulting extended addressing machines naturally model a weak call-by-name PCF with explicit substitutions. Finally, we show that they are also well suited for representing regular PCF programs (closed terms) computing natural numbers.
The quest for a fully abstract model of the call-by-value λ-calculus remains crucial in programming language theory, and constitutes an ongoing line of research. While a model enjoying this property has not been found yet, this interesting problem acts as a powerful motivation for investigating classes of models, studying the associated theories and capturing operational properties semantically. We study a relational model presented as a relevant intersection type system, where intersection is in general non-idempotent, except for an idempotent element that is injected in the system. This model is adequate, equates many λ-terms that are indeed equivalent in the maximal observational theory, and satisfies an Approximation Theorem w.r.t. a system of approximants representing finite pieces of call-by-value Böhm trees. We show that these tools can be used for characterizing the most significant properties of the calculus - namely valuability, potential valuability and solvability - both semantically, through the notion of approximants, and logically, by means of the type assignment system. We mainly focus on the characterizations of solvability, as they constitute an original result. Finally, we prove the decidability of the inhabitation problem for our type system by exhibiting a non-deterministic algorithm, which is proven sound, correct and terminating.
We study the two Girard's translations of intuitionistic implication into linear logic by exploiting the bang calculus, a paradigmatic functional language with an explicit box-operator that allows both the call-by-name and call-by-value λ-calculi to be encoded in. We investigate how the bang calculus subsumes both call-by-name and call-by-value λ-calculi from a syntactic and a semantic viewpoint.
The λ-calculus possesses a strong notion of extensionality, called "the ω-rule", which has been the subject of many investigations. It is a longstanding open problem whether the equivalence obtained by closing the theory of Böhm trees under the ω-rule is strictly included in Morris's original observational theory, as conjectured by Sallé in the seventies. In a recent work, Breuvart et al. have shown that Morris's theory satisfies the ω-rule. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture.
We study the theory of contextual equivalence in the untyped λ-calculus, generated by taking the normal forms as observables. Introduced by Morris in 1968, this is the original extensional λ-theory H+ of observational equivalence. On the syntactic side, we show that this λ-theory validates the ω-rule, thus settling a long-standing open problem. On the semantic side, we provide sufficient and necessary conditions for relational graph models to be fully abstract for H+. We show that a relational graph model captures Morris's observational pre-order exactly when it is extensional and λ-König. Intuitively, a model is λ-König when every λ-definable tree has an infinite path which is witnessed by some element of the model. Both results follows from a weak separability property enjoyed by terms differing only because of some infinite η-expansion, which is proved through a refined version of the Böhm-out technique.
We propose an algebraization of classical and non-classical logics, based on factor varieties and decomposition operators. In particular, we provide a new method for determining whether a propositional formula is a tautology or a contradiction. This method can be automatized by defining a term rewriting system that enjoys confluence and strong normalization. This also suggests an original notion of logical gate and circuit, where propositional variables becomes logical gates and logical operations are implemented by substitution. Concerning formulas with quantifiers, we present a simple algorithm based on factor varieties for reducing first-order classical logic to equational logic. We achieve a completeness result for first-order classical logic without requiring any additional structure.
We define the class of relational graph models and study the induced order- and equational-theories. Using the Taylor expansion, we show that all λ-terms with the same Böhm tree are equated in any relational graph model. If the model is moreover extensional and satisfies a technical condition, then its order-theory coincides with Morris's observational pre-order. Finally, we introduce an extensional version of the Taylor expansion, then prove that two λ-terms have the same extensional Taylor expansion exactly when they are equivalent in Morris's sense.
The category Rel of sets and relations yields one among the simplest denotational semantics of Linear Logic (LL). It is known that Rel is the biproduct completion of the Boolean ring. We consider the generalization of this construction to an arbitrary continuous semiring R, producing a cpo-enriched category which is a semantics of LL, and its (co)Kleisli category is an adequate model of an extension of PCF, parametrized by R. Specific instances of R allow us to compare programs not only with respect to "what they can do", but also "in how many steps" or "in how many different ways" (for non-deterministic PCF) or even "with what probability" (for probabilistic PCF).
We consider the call-by-value λ-calculus extended with a may-convergent non-deterministic choice and a must-convergent parallel composition. Inspired by recent works on the relational semantics of linear logic (LL) and non-idempotent intersection types, we endow this calculus with a type system based on the so-called Girard's second translation of intuitionistic logic into LL. We prove that a term is typable if and only if is converging, and that its typing tree carries enough information to give a bound on the length of its lazy call-by-value reduction. Moreover, when the typing tree is minimal, such a bound becomes the exact length of the reduction.
In simply typed λ-calculus with one ground type the following theorem due to Loader holds. (i) Given the full model F over a finite set, the question whether some element f∈F is λ-definable is undecidable. In the λ-calculus with intersection types based on countably many atoms, the following is proved by Urzyczyn. (ii) It is undecidable whether a type is inhabited. Both statements are major results presented in Barendregt-Dekkers-Statman'12. We show that (i) and (ii) follow from each other in a natural way, by interpreting intersection types as continuous functions logically related to elements of F. From this, and a result by Joly on λ-definability, we get that Urzyczyn's theorem already holds for intersection types with at most two atoms.
We present an abstract construction for building differential categories useful to model resource sensitive calculi, and we apply it to categories of games. In one instance, we recover a category previously used to give a fully abstract model of a nondeterministic imperative language. The construction exposes the differential structure already present in this model. A second instance corresponds to a new Cartesian differential category of games. We give a model of a Resource PCF in this category and show that it enjoys the finite definability property. Comparison with a relational semantics reveals that the latter also possesses this property and is fully abstract.
We study the resource calculus, an extension of the λ-calculus allowing to model resource consumption. We achieve an internal separation result, in analogy with Böhm's theorem of λ-calculus. We define an equivalence relation on the terms, which we prove to be the maximal non-trivial congruence on normalizable terms respecting β-reduction. It is significant that this equivalence extends the usual η-equivalence and is related to Ehrhard's Taylor expansion - a translation mapping terms into series of finite resources.
We study the semantics of a resource sensitive extension of the λ-calculus in a canonical reflexive object of a category of sets and relations, a relational version of the original Scott D∞ model of the pure λ-calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the λ-calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a 'must' parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary λ-calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula.
We provide a strong normalization result for MLF, a type system generalizing ML with first-class polymorphism as in system F. The proof is achieved by translating MLF into a calculus of coercions, and showing that this calculus is just a decorated version of system F.
We introduce the notion of differential λ-category as an extension of Blute-Cockett-Seely's differential Cartesian categories. We prove that differential λ-categories can be used to model the simply typed versions of: (i) the differential λ-calculus, a λ-calculus extended with a syntactic derivative operator; (ii) the resource calculus, a non-lazy axiomatisation of Boudol's λ-calculus with multiplicities. Finally, we provide two concrete examples of differential λ-categories, namely, the category MRel of sets and relations, and the category MFin of finiteness spaces and finitary relations.
We recently introduced an extensional model of the pure λ-calculus living in a cartesian closed category of sets and relations. In this paper, we provide sufficient conditions for categorical models living in arbitrary cpo-enriched cartesian closed categories to have H*, the maximal consistent sensible λ-theory, as their equational theory. Finally, we prove that our relational model fulfils these conditions.
We introduce the class of Church algebras, which is general enough to compass all Boolean algebras, Heyting algebras and rings with unit. Using a new equational characterization of central elements, we prove that Church algebras satisfy a Stone representation theorem. We show that every lattice of equational theories is isomorphic to the congruence lattice of a suitable Church algebra, and we use this property to prove a meta-Stone representation theorem which is applicable to all varieties of algebras.
We recently introduced an extensional model of the pure λ-calculus living in a canonical cartesian closed category of sets and relations. In the present paper, we study the non-deterministic features of this model. Unlike most traditional approaches, our way of interpreting non-determinism does not require any additional powerdomain construction: we show that our model provides a straightforward semantics of non-determinism (may convergence) by means of unions of interpretations as well as of parallelism (must convergence) by means of a binary, non-idempotent, operation available on the model, which is related to the mix rule of Linear Logic. More precisely, we introduce a λ-calculus extended with non-deterministic choice and parallel composition, and we define its operational semantics (based on the may and must intuitions underlying our two additional operations). We describe the interpretation of this calculus in our model and show that this interpretation is sensible with respect to our operational semantics: a term converges if, and only if, it has a non-empty interpretation.
We generalize to universal algebra concepts originating from λ-calculus and programming to prove a new result on the lattice λT of λ-theories, and a general theorem of pure universal algebra which can be seen as a meta version of the Stone Representation Theorem. In this paper we introduce the class of Church algebras (which includes all Boolean algebras, combinatory algebras, rings with unit and the term algebras of all λ-theories) to model the "if-then-else" instruction of programming. The interest of Church algebras is that each has a Boolean algebra of central elements, which play the role of the idempotent elements in rings. Central elements are the key tool to represent any Church algebra as a weak Boolean product of indecomposable Church algebras and to prove the meta representation theorem mentioned above. We generalize the notion of easy λ-term of lambda calculus to prove that any Church algebra with an 'easy set' of cardinality n admits (at the top) a lattice interval of congruences isomorphic to the free Boolean algebra with n generators. This theorem has the following consequence for the lattice of λ-theories: for every recursively enumerable λ-theory φ and each n, there is a λ-theory φn ≥ φ such that {ψ : ψ ≥ φn} 'is' the Boolean lattice with 2n elements.
Models of the untyped λ-calculus may be defined either as applicative structures satisfying a bunch of first-order axioms (λ-models), or as reflexive objects in cartesian closed categories (categorical models). In this paper we show that any categorical model of λ-calculus can be presented as a λ-model, even when the underlying category does not have enough points. We provide an example of an extensional model of λ-calculus in a category of sets and relations which has not enough points. Finally, we present some of its algebraic properties which make it suitable for dealing with non-deterministic extensions of λ-calculus.
A longstanding open problem is whether there exists a non-syntactical model of the untyped λ-calculus whose theory is exactly the least λ-theory λβ. In this paper we investigate the more general question of whether the equational/order theory of a model of the untyped λ-calculus can be recursively enumerable (r.e. for brevity). We introduce a notion of effective model of λ-calculus, which covers in particular all the models individually introduced in the literature. We prove that the order theory of an effective model is never r.e.; from this it follows that its equational theory cannot be λβ, λβη. We then show that no effective model living in the stable or strongly stable semantics has an r.e. equational theory. Concerning Scott's semantics, we investigate the class of graph models and prove that no order theory of a graph model can be r.e., and that there exists an effective graph model whose equational/order theory is the minimum one. Finally, we show that the class of graph models enjoys a kind of downwards Lowenheim-Skolem theorem.
In this paper we show that the Stone representation theorem for Boolean algebras can be generalized to combinatory algebras. In every combinatory algebra there is a Boolean algebra of central elements (playing the role of idempotent elements in rings), whose operations are defined by suitable combinators. Central elements are used to represent any combinatory algebra as a Boolean product of directly indecomposable combinatory algebras (i.e., algebras which cannot be decomposed as the Cartesian product of two other nontrivial algebras). Central elements are also used to provide applications of the representation theorem to lambda calculus. We show that the indecomposable semantics (i.e., the semantics of lambda calculus given in terms of models of lambda calculus, which are directly indecomposable as combinatory algebras) includes the continuous, stable and strongly stable semantics, and the term models of all semisensible lambda theories. In one of the main results of the paper we show that the indecomposable semantics is equationally incomplete, and this incompleteness is as wide as possible: for every recursively enumerable lambda theory T, there is a continuum of lambda theories including T which are omitted by the indecomposable semantics.
We discuss the real power of Ehrhard and Regnier's commutation result between Böhm trees and normalized Taylor expansion. It turns out that classic results like the contextuality of Böhm, syntactic continuity and the Parallel Lines Lemma can be given "soft" proofs by exploiting the main properties enjoyed by the resource calculus, namely strong normalization, confluence and linearity.
We study the two Girard's translations of intuitionistic implication into linear logic by exploiting the bang calculus, a paradigmatic functional language with an explicit box-operator that allows both the call-by-name and call-by value λ-calculi to be encoded in. We investigate how the bang calculus subsumes both call-by-name and call-by-value λ-calculi from a syntactic and a semantic viewpoint.
We provide a strong normalization result for MLF, a type system generalizing ML with first-class polymorphism as in system F. The proof is achieved by translating MLF into a calculus of coercions, and showing that this calculus is just a decorated version of system F. Simulation results then entail strong normalization from the same property of system F.
We describe preliminary investigation on Morris's original observational equivalence H+.
We present an algorithm for unifying untyped lambda terms.
| Davide Barbarossa | Taylor expansion for the λμ-calculus; |
| Flavien Breuvart | Non-standard observational equivalences; |
| Claudia Faggian | Abstract notions of Böhm trees; |
| Giulio Guerrieri | Abstract notions of Böhm trees; |
| Benedetto Intrigila | Computability theory |
| Axel Kerinec | Non-standard observational equivalences; Call-By-Value Lambda Calculus; |
| Simona Ronchi della Rocca | Call-By-Value Lambda Calculus. |
Home |
Teaching |
Curriculum |
Spare Time |
A mathematician is a machine for turning coffee into theorems.