Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userFunctional Pearl: The Distributive $lambda$-Calculus
73
0
0.0
(
0
)
Added by
Alejandro D\\'iaz-Caro
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We introduce a simple extension of the $lambda$-calculus with pairs---called the distributive $lambda$-calculus---obtained by adding a computational interpretation of the valid distributivity isomorphism $A Rightarrow (Bwedge C) equiv (ARightarrow B) wedge (ARightarrow C)$ of simple types. We study the calculus both as an untyped and as a simply typed setting. Key features of the untyped calculus are confluence, the absence of clashes of constructs, that is, evaluation never gets stuck, and a leftmost-outermost normalization theorem, obtained with straightforward proofs. With respect to simple types, we show that the new rules satisfy subject reduction if types are considered up to the distributivity isomorphism. The main result is strong normalization for simple types up to distributivity. The proof is a smooth variation over the one for the $lambda$-calculus with pairs and simple types.
rate research
Read More
This is a set of lecture notes that developed out of courses on the lambda calculus that I taught at the University of Ottawa in 2001 and at Dalhousie University in 2007 and 2013. Topics covered in these notes include the untyped lambda calculus, the Church-Rosser theorem, combinatory algebras, the simply-typed lambda calculus, the Curry-Howard isomorphism, weak and strong normalization, polymorphism, type inference, denotational semantics, complete partial orders, and the language PCF.
We introduce two extensions of the $lambda$-calculus with a probabilistic choice operator, $Lambda_oplus^{cbv}$ and $Lambda_oplus^{cbn}$, modeling respectively call-by-value and call-by-name probabilistic computation. We prove that both enjoys confluence and standardization, in an extended way: we revisit these two fundamental notions to take into account the asymptotic behaviour of terms. The common root of the two calculi is a further calculus based on Linear Logic, $Lambda_oplus^!$, which allows for a fine control of the interaction between choice and copying, and which allows us to develop a unified, modular approach.
We study polymorphic type assignment systems for untyped lambda-calculi with effects, based on Moggis monadic approach. Moving from the abstract definition of monads, we introduce a version of the call-by-value computational lambda-calculus based on Wadlers variant with unit and bind combinators, and without let. We define a notion of reduction for the calculus and prove it confluent, and also we relate our calculus to the original work by Moggi showing that his untyped metalanguage can be interpreted and simulated in our calculus. We then introduce an intersection type system inspired to Barendregt, Coppo and Dezani system for ordinary untyped lambda-calculus, establishing type invariance under conversion, and provide models of the calculus via inverse limit and filter model constructions and relate them. We prove soundness and completeness of the type system, together with subject reduction and expansion properties. Finally, we introduce a notion of convergence, which is precisely related to reduction, and characterize convergent terms via their types.
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs, but for the first time admit an adequacy theorem relating the operational and denotational views. This resolves the main issue left open in (Bacci et al. 2018).
In this paper we briefly summarize the contents of Manzonettos PhD thesis which concerns denotational semantics and equational/order theories of the pure untyped lambda-calculus. The main research achievements include: (i) a general construction of lambda-models from reflexive objects in (possibly non-well-pointed) categories; (ii) a Stone-style representation theorem for combinatory algebras; (iii) a proof that no effective lambda-model can have lambda-beta or lambda-beta-eta as its equational theory (this can be seen as a partial answer to an open problem introduced by Honsell-Ronchi Della Rocca in 1984).
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
