اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدLecture notes on the lambda calculus
195
0
0.0
(
0
)
تأليف
Peter Selinger
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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.
قيم البحث
اقرأ أيضاً
These informal lecture notes describe the progress in semiconductor spintronics in a historic perspective as well as in a comparison to achievements of spintronics of ferromagnetic metals. After outlining motivations behind spintronic research, selec
ted results of investigations on three groups of materials are presented. These include non-magnetic semiconductors, hybrid structures involving semiconductors and ferromagnetic metals, and diluted magnetic semiconductors either in paramagnetic or ferromagnetic phase. Particular attention is paid to the hole-controlled ferromagnetic systems whose thermodynamic, micromagnetic, transport, and optical properties are described in detail together with relevant theoretical models.
These lecture notes have been developed for the course Computational Social Choice of the Artificial Intelligence MSc programme at the University of Groningen. They cover mathematical and algorithmic aspects of voting theory.
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.
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 conflu
ence 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.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
