Ang Lambda calculus ay isang pormal na sistema sa mathematical logic para sa pagpapahayag ng abstraction-based na mga kalkulasyon at paglalapat ng mga function gamit ang binding at variable substitution. Ito ay isang unibersal na modelo na maaaring ilapat sa disenyo ng anumang Turing machine. Ang lambda calculus ay unang ipinakilala ni Church, isang sikat na mathematician, noong 1930s.
Binubuo ang system ng pagbuo ng mga miyembro ng lambda at pagsasagawa ng mga reduction operation sa kanila.
Mga Pagpapaliwanag at Aplikasyon
Ang letrang Griyego na lambda (λ) ay ginagamit sa mga expression ng lambda at termino ng lambda upang tukuyin ang pagbubuklod ng isang variable sa isang function.
Lambda calculus ay maaaring i-untype o i-type. Sa unang variant, magagamit lang ang mga function kung kaya nilang tumanggap ng ganitong uri ng data. Ang na-type na lambda calculi ay mas mahina, maaaring magpahayag ng mas maliit na halaga. Ngunit, sa kabilang banda, pinapayagan ka nitong patunayan ang higit pang mga bagay.
Isang dahilan kung bakit napakaraming iba't ibang uri ay ang pagnanais ng mga siyentipiko na gumawa ng higit pa nang hindi binibitiwan ang pagkakataong patunayan ang matibay na teorema ng lambda calculus.
May mga aplikasyon ang system sa maraming iba't ibang larangan ng matematika, pilosopiya, lingguwistika, at computer science. Una sa lahat, ang lambda calculus ay isang calculus na may mahalagang papel sa pagbuo ng teorya ng mga programming language. Ito ang mga istilo ng functional na paglikha na ipinapatupad ng mga system. Isa rin silang mainit na paksa ng pananaliksik sa teorya ng mga kategoryang ito.
Para sa mga dummies
Ang lambda calculus ay ipinakilala ng mathematician na Alonzo Church noong 1930s bilang bahagi ng kanyang pananaliksik sa mga pundasyon ng agham. Ang orihinal na sistema ay ipinakitang lohikal na hindi naaayon noong 1935 nang si Stephen Kleen at J. B. Rosser ay bumuo ng Kleene-Rosser paradox.
Mamaya, noong 1936, pinili at inilathala ng Simbahan ang bahagi lamang na nauugnay sa mga kalkulasyon, ang tinatawag ngayong hindi na-type na lambda calculus. Noong 1940 ay ipinakilala rin niya ang isang mas mahina ngunit lohikal na pare-parehong teorya na kilala bilang ang sistema ng pangunahing uri. Sa kanyang trabaho, ipinaliwanag niya ang buong teorya sa mga simpleng salita, kaya masasabing inilathala ng Simbahan ang calculus lambda para sa mga dummies.
Hanggang noong 1960s, nang maging malinaw ang kaugnayan nito sa mga programming language, ang λ ay isang pormalismo lamang. Salamat sa mga aplikasyon ni Richard Montagu at iba pang mga linguist sa semantics ng natural na wika, ang calculus ay nagkaroon ng pagmamalaki sa parehong linguistics at computer science.
Pinagmulan ng simbolo
Ang Lambda ay hindi kumakatawan sa isang salita o acronym, ito ay nagmula sa isang reference sa Russell's Principal Mathematics na sinusundan ng dalawang typographical na pagbabago. Halimbawa ng notasyon: para sa isang function na f na may f (y)=2y + 1 ay 2ŷ + 1. At dito gumagamit kami ng caret (“sumbrero”) sa ibabaw ng y upang lagyan ng label ang input variable.
Ang simbahan ay orihinal na nilayon na gumamit ng mga katulad na simbolo, ngunit hindi nailagay ng mga typesetter ang simbolo ng "sombrero" sa itaas ng mga titik. Kaya sa halip ay orihinal nilang na-print ito bilang "/\y.2y+1". Sa susunod na yugto ng pag-edit, pinalitan ng mga typist ang "/ \" ng isang karakter na nakikitang katulad.
Introduction to lambda calculus
Binubuo ang system ng isang wika ng mga termino, na pinipili ng isang partikular na pormal na syntax, at isang hanay ng mga panuntunan sa pagbabagong-anyo na nagpapahintulot sa kanila na manipulahin. Ang huling punto ay maaaring ituring bilang isang equational theory o bilang isang operational definition.
Lahat ng function sa lambda calculus ay anonymous, ibig sabihin ay wala silang mga pangalan. Isang input variable lang ang kinukuha nila, at ginagamit ang currying para ipatupad ang mga plot na may maraming variable.
Lambda terms
Tinutukoy ng calculus syntax ang ilang expression bilang wasto at ang iba ay hindi wasto. Tulad ng iba't ibang mga string ng mga character ay wastong C program at ang ilan ay hindi. Ang aktwal na expression ng lambda calculus ay tinatawag na "lambda term".
Ang sumusunod na tatlong panuntunan ay nagbibigay ng pasaklaw na kahulugan na maaaringilapat sa pagbuo ng lahat ng syntactically valid na konsepto:
Ang x variable mismo ay isang wastong termino ng lambda:
- kung ang T ay LT at ang x ay non-constant, kung gayon ang (lambda xt) ay tinatawag na abstraction.
- kung ang T pati na rin ang s ay mga konsepto, ang (TS) ay tinatawag na aplikasyon.
Wala nang iba pang terminong lambda. Kaya, ang isang konsepto ay wasto kung at kung ito ay makukuha lamang sa pamamagitan ng paulit-ulit na aplikasyon ng tatlong panuntunang ito. Gayunpaman, maaaring tanggalin ang ilang bracket ayon sa iba pang pamantayan.
Definition
Ang mga expression ng Lambda ay binubuo ng:
- variables v 1, v 2, …, v n, …
- mga simbolo ng abstraction na 'λ' at tuldok '.'
- bracket ().
Ang hanay na Λ ay maaaring tukuyin nang pasaklaw:
- Kung ang x ay isang variable, kung gayon ang x ∈ Λ;
- x ay hindi pare-pareho at M ∈ Λ, pagkatapos ay (λx. M) ∈ Λ;
- M, N ∈ Λ, pagkatapos ay (MN) ∈ Λ.
Designation
Upang panatilihing walang kalat ang notasyon ng mga expression ng lambda, karaniwang ginagamit ang mga sumusunod na convention:
- Inalis ang mga panlabas na bracket: MN sa halip na (MN).
- Ang mga application ay ipinapalagay na mananatiling nauugnay: maaaring isulat ng isa ang MNP sa halip na ((MN) P).
- Ang katawan ng abstraction ay umaabot sa kanan: λx. MN ay nangangahulugang λx. (MN), hindi (λx. M) N.
- Nababawasan ang pagkakasunod-sunod ng mga abstraction: λx.λy.λz. N ay maaaring λxyz. N.
Mga libre at nakatali na variable
Ikinokonekta ng operator na λ ang hindi-constant nito saanman ito naroroon sa katawan ng abstraction. Ang mga variable na nahuhulog sa saklaw ay tinatawag na bound. Sa expression na λ x. M, ang λ x na bahagi ay madalas na tinutukoy bilang isang panali. Na parang nagpapahiwatig na ang mga variable ay magiging isang pangkat na may pagdaragdag ng X x sa M. Ang lahat ng iba pang hindi matatag ay tinatawag na libre.
Halimbawa, sa expression na λ y. x y, y - hindi permanenteng nakatali, at x - libre. At nararapat ding tandaan na ang variable ay naka-grupo ayon sa "pinakamalapit" nitong abstraction. Sa sumusunod na halimbawa, ang lambda calculus solution ay kinakatawan ng isang paglitaw ng x, na nauugnay sa pangalawang termino:
λ x. y (λ x. z x)
Ang hanay ng mga libreng variable na M ay tinutukoy bilang FV (M) at tinukoy sa pamamagitan ng pag-uulit sa istruktura ng mga termino gaya ng sumusunod:
- FV (x)={x}, kung saan ang x ay isang variable.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Ang isang formula na hindi naglalaman ng mga libreng variable ay tinatawag na sarado. Ang mga closed lambda expression ay kilala rin bilang mga combinator at katumbas ng mga termino sa combinatorial logic.
Abbreviation
Natutukoy ang kahulugan ng mga expression ng lambda sa pamamagitan ng kung paano paikliin ang mga ito.
May tatlong uri ng cut:
- α-transform: pagpapalit ng mga nakatali na variable (alpha).
- β-reduction: paglalapat ng mga function sa kanilang mga argumento (beta).
- η-transform: sumasaklaw sa paniwala ng extensionality.
Narito rinpinag-uusapan natin ang mga resultang equivalence: dalawang expression ay β-equivalent kung maaari silang β-transformed sa parehong component, at ang α / η-equivalence ay parehong tinukoy.
Ang terminong redex, na maikli para sa reducible turnover, ay tumutukoy sa mga subtopic na maaaring bawasan ng isa sa mga panuntunan. Lambda calculus para sa mga dummies, mga halimbawa:
Ang (λ x. M) N ay isang beta redex sa expression para sa pagpapalit ng N ng x sa M. Ang bahagi kung saan binabawasan ang isang redex ay tinatawag na reduct nito. Ang pagbabawas (λ x. M) N ay M [x:=N].
Kung ang x ay hindi libre sa M, λ x. M x din em-REDEX na may regulator M.
α-transformation
Binibigyang-daan ka ng Alpha rename na baguhin ang mga pangalan ng mga nakatali na variable. Halimbawa, x. x ay maaaring magbigay ng λ y. y. Ang mga terminong nagkakaiba lamang sa alpha transformation ay sinasabing α-equivalent. Kadalasan, kapag gumagamit ng lambda calculus, ang α-equivalents ay itinuturing na katumbas.
Ang eksaktong mga panuntunan para sa alpha conversion ay hindi lubos na mahalaga. Una, sa abstraction na ito, tanging ang mga variable na nauugnay sa parehong system ang pinalitan ng pangalan. Halimbawa, ang alpha transform λ x.λ x. x ay maaaring humantong sa λ y.λ x. x, ngunit maaaring hindi ito humantong sa λy.λx.y Ang huli ay may ibang kahulugan kaysa sa orihinal. Ito ay kahalintulad sa konsepto ng variable shadowing programming.
Pangalawa, hindi posible ang alpha transform kung magreresulta ito sa pagkuha ng isang hindi permanenteng abstraction. Halimbawa, kung papalitan mo ang x ng y sa λ x.λ y. x, pagkatapos ay maaari mong makuhaλy.λy. u, na hindi pareho.
Sa mga programming language na may static na saklaw, ang alpha conversion ay maaaring gamitin upang pasimplehin ang resolution ng pangalan. Kasabay nito, ang pag-iingat na ang konsepto ng isang variable ay hindi nakatago sa pagtatalaga sa naglalaman ng lugar.
Sa De Bruyne index notation, anumang dalawang alpha-equivalent terms ay syntactically identical.
Palitan
Ang mga pagbabagong isinulat ni E [V:=R] ay ang proseso ng pagpapalit ng lahat ng libreng paglitaw ng variable na V sa expression na E sa turnover na R. Ang pagpapalit sa mga tuntunin ng λ ay tinukoy ng lambda ng recursion calculus sa istraktura ng konsepto tulad ng sumusunod (tandaan: x at y - mga variable lamang, at M at N - anumang λ-expression).
x [x:=N] ≡ N
y [x:=N] ≡ y kung x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) kung x ≠ y, sa kondisyon na y ∉ FV (N).
Para sa pagpapalit sa isang lambda abstraction, minsan ay kinakailangan na α-transform ang isang expression. Halimbawa, hindi totoo na ang (λ x. Y) [y:=x] ay nagreresulta sa (λ x. X) dahil ang pinalit na x ay dapat na libre, ngunit nauwi sa pagkakatali. Ang tamang kapalit sa kasong ito ay (λ z. X) hanggang sa α-equivalence. Tandaan na ang pagpapalit ay natatanging tinukoy hanggang sa lambda.
β-reduction
Ang Beta reduction ay sumasalamin sa ideya ng paglalapat ng isang function. Ang beta-reductive ay tinukoy sa mga terminopagpapalit: ((X V. E) E ') ay E [V:=E'].
Halimbawa, kung ipagpalagay na ang ilang encoding 2, 7, ×, mayroong sumusunod na β-reduction: ((λ n. N × 2) 7) → 7 × 2.
Ang pagbabawas ng beta ay makikita na kapareho ng konsepto ng local reducibility sa ilalim ng natural na bawas sa pamamagitan ng Curry-Howard isomorphism.
η-transform
Ang conversion na ito ay nagpapahayag ng ideya ng extension, na sa kontekstong ito ay ang dalawang function ay pantay-pantay kapag nagbibigay sila ng parehong resulta para sa lahat ng argumento. Ang conversion na ito ay nagpapalitan sa pagitan ng λ x. (F x) at f sa tuwing ang x ay mukhang hindi libre sa f.
Ang pagkilos na ito ay maaaring ituring na kapareho ng konsepto ng lokal na pagkakumpleto sa natural na bawas sa pamamagitan ng Curry-Howard isomorphism.
Mga normal na anyo at pagsasanib
Para sa isang hindi na-type na lambda calculus, ang panuntunan ng β-reduction ay karaniwang hindi malakas o mahinang normalizing.
Gayunpaman, maipapakita na ang β-reduction ay nagsasama kapag tumatakbo bago ang α-transformation (ibig sabihin, dalawang normal na anyo ang maaaring ituring na pantay-pantay kung posible ang isang α-transformation mula sa isa patungo sa isa pa).
Samakatuwid, parehong may iisang normal na anyo ang mga terminong malakas sa pag-normalize at mahinang pagsasaayos. Para sa mga unang termino, ang anumang diskarte sa pagbabawas ay garantisadong magreresulta sa isang karaniwang pagsasaayos. Samantalang para sa mahinang pag-normalize ng mga kondisyon, maaaring hindi ito mahanap ng ilang diskarte sa pagbabawas.
Mga karagdagang pamamaraan ng programming
Maraming idiom ng paglikha para sa lambda calculus. Marami sa kanila ay orihinal na binuo sa konteksto ng paggamit ng mga system bilang batayan para sa mga semantika ng isang programming language, na epektibong inilalapat ang mga ito bilang isang mababang antas na konstruksyon. Dahil ang ilang mga istilo ay may kasamang lambda calculus (o isang bagay na halos kapareho) bilang isang snippet, ang mga diskarteng ito ay magagamit din sa praktikal na paggawa, ngunit maaaring maisip na malabo o banyaga.
Named constants
Sa lambda calculus, ang isang library ay nasa anyo ng isang set ng mga dating tinukoy na function, kung saan ang mga termino ay mga konkretong constants lamang. Ang purong calculus ay walang konsepto ng pinangalanang immutable dahil ang lahat ng atomic lambda terms ay variables. Ngunit maaari rin silang gayahin sa pamamagitan ng pagkuha sa mutable bilang pangalan ng constant, gamit ang lambda abstraction upang itali ang pabagu-bago ng isip sa katawan, at paglalapat ng abstraction na iyon sa nilalayon na kahulugan. Kaya kung gagamit ka ng f upang kumatawan sa M sa N, masasabi mong
(λ f. N) M.
Madalas na ipinakilala ng mga may-akda ang isang konseptong sintaktik tulad ng hayaan na payagan ang mga bagay na maisulat sa mas intuitive na paraan.
f=M hanggang N
Sa pamamagitan ng pag-chaining ng mga naturang kahulugan, maaaring magsulat ang isang lambda calculus na "program" bilang zero o higit pang mga kahulugan ng function na sinusundan ng isang miyembro ng lambda, gamit ang mga kahulugang iyon na bumubuo sa karamihan ng program.
Ang isang kapansin-pansing limitasyon ng let na ito ay ang pangalang f ay hindi tinukoy sa M,dahil ang M ay nasa labas ng umiiral na saklaw ng lambda abstraction f. Nangangahulugan ito na ang isang recursive function na attribute ay hindi maaaring gamitin bilang M na may let. Ang mas advanced na letrec syntax, na nagbibigay-daan sa iyong magsulat ng mga recursive function na kahulugan sa istilong ito, ay gumagamit ng mga fixed-point combinator sa halip.
Mga naka-print na analogue
Ang uri na ito ay isang naka-type na pormalismo na gumagamit ng simbolo upang kumatawan sa isang anonymous na abstraction ng function. Sa kontekstong ito, ang mga uri ay karaniwang mga bagay na may likas na syntactic na itinalaga sa mga termino ng lambda. Ang eksaktong kalikasan ay nakasalalay sa calculus na pinag-uusapan. Mula sa isang tiyak na punto ng view, ang nai-type na LI ay maaaring ituring bilang mga pagpipino ng hindi na-type na LI. Ngunit sa kabilang banda, maaari rin silang ituring na isang mas pangunahing teorya, at ang hindi na-type na lambda calculus ay isang espesyal na kaso na may isang uri lamang.
Ang Typed LI ay ang pundasyon ng mga programming language at ang backbone ng functional na mga wika gaya ng ML at Haskell. At, higit na hindi tuwiran, mga mahalagang istilo ng paglikha. Ang na-type na lambda calculi ay may mahalagang papel sa pagbuo ng mga uri ng system para sa mga programming language. Dito, karaniwang kinukuha ng typability ang mga gustong katangian ng program, halimbawa, hindi ito magdudulot ng paglabag sa pag-access sa memorya.
Ang Typed lambda calculi ay malapit na nauugnay sa mathematical logic at proof theory sa pamamagitan ng Curry–Howard isomorphism, at maaaring ituring bilang isang panloob na wika ng mga klase ng kategorya, halimbawa, naSimple lang ang istilo ng mga pagsasara ng Cartesian.
