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 Boehm(-like) tree and a theory of program approximation in the call-by-value setting. We prove that all lambda terms having the same Bohm tree are observationally equivalent, and characterize those Boehm-like trees arising as actual Boehm 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 Boehm tree. From this it follows that two lambda terms have the same Boehm 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 Boehm 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.
ML^{F} 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 ML^{F} 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 xML^{F}, the Church-style version of ML^{F}, 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 xML^{F} through the same property of system F. We then transfer the result to all other versions of ML^{F} using the fact that they can be compiled into xML^{F} 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.
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 Boehm 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 Boehm 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 Boehm'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 ML^{F}, a type system generalizing ML with first-class polymorphism as in system F. The proof is achieved by translating ML^{F} 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 2^{n} 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 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 ML^{F}, a type system generalizing ML with first-class polymorphism as in system F. The proof is achieved by translating ML^{F} 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.
Thomas Ehrhard | Call-By-Push-Value Relational Models; |
Giulio Guerrieri | Call-By-Push-Value Relational Models; |
Stefano Guerrini | Goedel's koan |
Benedetto Intrigila | Goedel's koan |
Jim Laird | Quantitative models of nondeterministic PCF; |
Guy McCusker | Quantitative models of nondeterministic PCF; |
Michele Pagani | Quantitative models of nondeterministic PCF; |
Andrew Polonsky | Lambda Calculus: Double fixed point combinators and Unification |
Simona Ronchi della Rocca | Call-By-Value Weak Lambda Calculus. |
Antonino Salibra | Algebraization of Logics based on Decomposition operators. |
Home |
Teaching |
Curriculum |
Spare Time |
A mathematician is a machine for turning coffee into theorems.