حساب لمبدا

(تم التحويل من تحليل لمبدا)

في علم الحاسوب النظري والرياضيات، تحليل لمبدا (الإنكليزية: Lambda calculus وأيضاً تكتب λ-calculus)، هو عبارة عن نظام شكلي لتعريف التوابع وتطبيق التوابع والاستدعاء الذاتي recursion. قدمت لأول مرة من قبل ألونزو تشرش في ثلاثينيات القرن العشرين كجزء من محاولة لوضع أسس الرياضيات.[1][2]

After the original system was shown to be logically inconsistent (the Kleene-Rosser paradox), Church isolated and published in 1936[3] 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.[4] 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.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

انظر أيضاً


الهامش والمراجع

  1. ^ A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).
  2. ^ For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
  3. ^ A. Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, Volume 58, No. 2. (Apr., 1936), pp. 345-363.
  4. ^ A. Church, "A Formulation of the Simple Theory of Types", Journal of Symbolic Logic, Volume 5 (1940).

للاستزادة

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.

وصلات خارجية

الكلمات الدالة: