حساب لمبدا
في فهم الحاسوب النظري والرياضيات، تحليل لمبدا (الإنكليزية: Lambda calculus وأيضاً تخط λ-calculus)، هوتعبير عن نظام شكلي لتعريف التوابع وتطبيق التوابع والاستنادىء الذاتي recursion. قدمت لأول مرة من قبل ألونزوتشرش في ثلاثينيات القرن العشرين كجزء من محاولة لوضع أسس الرياضيات.
After the original system was shown to be logically inconsistent (the Kleene-Rosser paradox), Church isolated and published in 1936 just the portion relevant to computation, what is now called the untyped lambda calculus. In 1940, he also introduced a computationally weaker but logically consistent system, known as the simply typed lambda calculus. In both typed and untyped versions, ideas from lambda calculus have found application in the fields of logic, recursion theory (computability), and linguistics, and have played an important role in the development of the theory of programming languages (with untyped lambda calculus being the original inspiration for functional programming, in particular Lisp, and typed lambda calculi serving as the foundation for modern type systems). This article deals primarily with the untyped lambda calculus.
انظر أيضاً
- Applicative computing systems – Treatment of objects in the style of the lambda calculus
- Binary Lambda Calculus – A version of lambda calculus with binary I/O, a binary encoding of terms, and a designated universal machine.
- Calculus of constructions – A typed lambda calculus with types as first-class values
- Cartesian closed category – A setting for lambda calculus in category theory
- Categorical abstract machine – A model of computation applicable to lambda calculus
- Combinatory logic – A notation for mathematical logic without variables
- Curry-Howard isomorphism – The formal correspondence between programs and proofs
- Domain theory – Study of certain posets giving denotational semantics for lambda calculus
- Evaluation strategy – Rules for the evaluation of expressions in programming languages
- Explicit substitution – The theory of substitution, as used in β-reduction
- Harrop formula – A kind of constructive logical formula such that proofs are lambda terms
- Kleene-Rosser paradox – A demonstration that some form of lambda calculus is inconsistent
- Knights of the Lambda Calculus – A semi-fictional organization of LISP and Scheme hackers
- Lambda cube – A framework for some extensions of typed lambda calculus
- Lambda-mu calculus – An extension of the lambda calculus for treating classical logic
- Rewriting – Transformation of formulæ in formal systems
- SECD machine – A virtual machine designed for the lambda calculus
- SKI combinator calculus – A computational system based on the S, K and I combinators
- System F – A typed lambda calculus with type-variables
- Typed lambda calculus – Lambda calculus with typed variables (and functions)
- Unlambda – An esoteric functional programming language based on combinatory logic
الهامش والمراجع
- ^ A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).
- ^ For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
- ^ A. Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, Volume 58, No. 2. (Apr., 1936), pp. 345-363.
- ^ A. Church, "A Formulation of the Simple Theory of Types", Journal of Symbolic Logic, Volumeخمسة (1940).
للاستزادة
- Abelson, Harold & Gerald Jay Sussman. Structure and Interpretation of Computer Programs. The MIT Press. ISBN 0-262-51087-1.
- Hendrik Pieter Barendregt .
- Henk Barendregt, The Impact of the Lambda Calculus in Logic and Computer Science. The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997.
- Barendregt, Hendrik Pieter, The Type Free Lambda Calculus pp1091–1132 of Handbook of Mathematical Logic, North-Holland (1977) ISBN 0-7204-2285-X
- Cardone and Hindley, 2006. History of Lambda-calculus and Combinatory Logic. In Gabbay and Woods (eds.), Handbook of the History of Logic, vol. 5. Elsevier.
- Church, Alonzo, An unsolvable problem of elementary number theory, American Journal of Mathematics, 58 (1936), pp. 345-363. This paper contains the proof that the equivalence of lambda expressions is in general not decidable.
- Kleene, Stephen, A theory of positive integers in formal logic, American Journal of Mathematics, 57 (1935), pp. 153-173 and 219-244. Contains the lambda calculus definitions of several familiar functions.
- Landin, Peter, A Correspondence Between ALGOL 60 and Church's Lambda-Notation, Communications of the ACM, vol. 8, no. 2 (1965), pages 89–101. Available from the ACM site. A classic paper highlighting the importance of lambda calculus as a basis for programming languages.
- Larson, Jim, . A gentle introduction for programmers.
- Schalk, A. and Simmons, H. (2005) An introduction to λ-calculi and arithmetic with a decent selection of exercises. Notes for a course in the Mathematical Logic MSc at Manchester University.
- de Queiroz, Ruy J.G.B. (2008) . Studia Logica, 90(2):211-247. A paper giving a formal underpinning to the idea of ‘meaning-is-use’ which, even if based on proofs, it is different from proof-theoretic semantics as in the Dummett–Prawitz tradition since it takes reduction as the rules giving meaning.
Monographs/textbooks for graduate students:
- Morten Heine Sørensen, Paweł Urzyczyn, Lectures on the Curry-Howard isomorphism, Elsevier, 2006, ISBN 0-444-52077-5 is a recent monograph that covers the main topics of lambda calculus from the type-free variety, to most typed lambda calculi, including more recent developments like pure type systems and the lambda cube. It does not cover subtyping extensions.
- Pierce, Benjamin (2002), Types and Programming Languages, MIT Press, ISBN 0-262-16209-1 covers lambda calculi from a practical type system perspective; some topics like dependent types are only mentioned, but subtyping is an important topic.
Some parts of this article are based on material from FOLDOC, used with permission.
وصلات خارجية
- Achim Jung, A Short Introduction to the Lambda Calculus-(PDF)
- David C. Keenan, To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction
- Raúl Rojas, A Tutorial Introduction to the Lambda Calculus-(PDF)
- Peter Selinger, Lecture Notes on the Lambda Calculus-(PDF)
- L. Allison, Some executable λ-calculus examples
- Chris Barker, Some executable (Javascript) simple examples, and text.
- Georg P. Loczewski,
- Bret Victor, Alligator Eggs: A Puzzle Game Based on Lambda Calculus
- Lambda Calculus on Safalra’s Website
- Lambda Calculus على بلانيت ماث
- LCI Lambda Interpreter a simple yet powerful pure calculus interpreter
- Lambda Calculus links on Lambda-the-Ultimate
- Mike Thyer, Lambda Animator, a graphical Java applet demonstrating alternative reduction strategies.
- An Introduction to Lambda Calculus and Scheme, by Jim Larson
