Ламбда тооцоолол нь хийсвэрлэлд суурилсан тооцооллыг илэрхийлэх, холбох болон хувьсах орлуулалтыг ашиглан функцуудыг ашиглахад зориулагдсан математик логикийн албан ёсны систем юм. Энэ бол ямар ч Тьюрингийн машины загварт хэрэглэж болох бүх нийтийн загвар юм. Ламбдагийн тооцоог 1930-аад онд алдарт математикч Черч анх нэвтрүүлсэн.
Систем нь ламбда гишүүдийг барьж, тэдгээр дээр багасгах үйлдлүүдээс бүрдэнэ.
Тайлбар ба өргөдөл
Грек үсгийг lambda (λ) нь lambda илэрхийлэл болон lambda нэр томъёонд хэрэглэгддэг бөгөөд функц дэх хувьсагчийг холбохыг илэрхийлдэг.
Ламбда тооцооллыг задлах эсвэл бичих боломжтой. Эхний хувилбарт функцийг зөвхөн ийм төрлийн өгөгдлийг хүлээн авах боломжтой тохиолдолд л ашиглах боломжтой. Бичсэн ламбда чулуу нь сул, бага утгыг илэрхийлж чаддаг. Гэхдээ нөгөө талаас тэд танд илүү олон зүйлийг нотлох боломжийг олгодог.
Тийм олон төрөл байдгийн нэг шалтгаан нь эрдэмтэд ламбда тооцооллын хүчтэй теоремуудыг батлах боломжоо орхихгүйгээр илүү ихийг хийх хүсэл юм.
Систем нь математик, философи, хэл шинжлэл, компьютерийн шинжлэх ухааны олон салбарт хэрэглэгдэхүүнтэй. Юуны өмнө lambda тооцоолол нь програмчлалын хэлний онолыг хөгжүүлэхэд чухал үүрэг гүйцэтгэсэн тооцоолол юм. Энэ нь системийн хэрэгжүүлдэг функциональ бүтээлийн хэв маяг юм. Эдгээр нь мөн эдгээр ангиллын онолын судалгааны халуун сэдэв юм.
Даммигийн хувьд
Хамбагийн тооцоог математикч Алонзо Сүм 1930-аад онд шинжлэх ухааны үндэс суурийг судлах ажлынхаа хүрээнд нэвтрүүлсэн. Анхны систем нь 1935 онд Стивен Клин, Ж. Б. Россер нар Клин-Россерын парадоксыг бий болгох үед логикийн хувьд зөрчилтэй болохыг харуулсан.
Хожим нь, 1936 онд Черч зөвхөн тооцоололд хамаарах хэсгийг онцолж нийтэлсэн бөгөөд үүнийг одоо төрөлжөөгүй ламбда тооцоо гэж нэрлэдэг. 1940 онд тэрээр мөн үндсэн төрлийн систем гэж нэрлэгддэг сул боловч логикийн хувьд нийцтэй онолыг нэвтрүүлсэн. Тэрээр бүтээлдээ онолыг бүхэлд нь энгийн үгээр тайлбарласан тул Сүм дамми нарт зориулсан ламбда тооцоололыг нийтэлсэн гэж хэлж болно.
1960-аад он хүртэл програмчлалын хэлтэй холбоотой нь тодорхой болох үед λ зүгээр л формализм байсан. Ричард Монтагу болон бусад хэл шинжлэлийн судлаачдын байгалийн хэлний семантикт хэрэглэсний ачаар тооцоолол нь хэл шинжлэл, компьютерийн шинжлэх ухаанд ч бахархалтай байр суурь эзэлдэг.
Бэлгэ тэмдгийн гарал үүсэл
Ламбда гэдэг нь нэг үг эсвэл товчилсон нэрийн товчлол биш бөгөөд энэ нь Расселын Үндсэн Математикийн эшлэлээс гаралтай бөгөөд дараа нь хоёр бичгийн хэв өөрчлөгдсөн. Тэмдэглэгээний жишээ: f (y)=2y + 1-тэй f функцийн хувьд 2ŷ + 1 байна. Энд бид оролтын хувьсагчийг шошголохдоо y-ийн дээгүүр тэмдэг (“малгай”) ашигладаг.
Сүм анх ижил төстэй тэмдэглэгээг ашиглах зорилготой байсан ч бичээчид "малгай" тэмдгийг үсгүүдийн дээр байрлуулж чадаагүй. Тиймээс тэд үүнийг анх "/\y.2y+1" гэж хэвлэсэн. Засварлах дараагийн ангид бичигчид "/ \"-г харагдахуйц төстэй тэмдэгтээр сольсон.
Ламбда тооцооллын танилцуулга
Систем нь тодорхой албан ёсны синтаксаар сонгогдсон нэр томьёоны хэл, тэдгээрийг өөрчлөх боломжийг олгодог хувиргах дүрмүүдээс бүрдэнэ. Сүүлийн цэгийг тэгшитгэлийн онол эсвэл үйл ажиллагааны тодорхойлолт гэж үзэж болно.
Ламбда тооцооллын бүх функцууд нэргүй бөгөөд тэдгээрт нэр байхгүй гэсэн үг. Тэд зөвхөн нэг оролтын хувьсагчийг авдаг бөгөөд карриинг нь олон хувьсагчтай графикийг хэрэгжүүлэхэд ашиглагддаг.
Ламбда нөхцөл
Тооцооллын синтакс нь зарим илэрхийллийг хүчинтэй, заримыг хүчингүй гэж тодорхойлдог. Яг л өөр өөр тэмдэгтийн мөрүүд нь C программууд хүчинтэй байдаг, зарим нь тийм биш байдаг шиг. Ламбда тооллын бодит илэрхийллийг "ламбда нэр томъёо" гэж нэрлэдэг.
Дараах гурван дүрэм нь байж болох индуктив тодорхойлолтыг өгдөгсинтаксийн хувьд хүчинтэй бүх ухагдахууныг бүтээхэд хэрэглэнэ:
X хувьсагч нь өөрөө хүчинтэй lambda нэр томъёо юм:
- хэрэв T нь LT, x нь тогтмол биш бол (lambda xt) хийсвэрлэл гэж нэрлэдэг.
- хэрэв T болон s нь ойлголт бол (TS) программ гэж нэрлэгддэг.
Өөр юу ч бол ламбда гэсэн нэр томъёо биш. Иймээс үзэл баримтлал нь эдгээр гурван дүрмийг давтан хэрэглэх замаар олж авах боломжтой тохиолдолд л хүчинтэй болно. Гэсэн хэдий ч бусад шалгуурын дагуу зарим хаалтыг орхигдуулж болно.
Тодорхойлолт
Ламбда илэрхийлэл нь:
- хувьсагч v 1, v 2, …, v n, …
- хийсвэрлэлийн 'λ' ба цэгийн тэмдэг.'
- хаалт ().
Λ олонлогийг индуктив байдлаар тодорхойлж болно:
- Хэрэв x нь хувьсагч бол x ∈ Λ;
- x тогтмол биш ба M ∈ Λ, тэгвэл (λx. M) ∈ Λ;
- M, N ∈ Λ, дараа нь (MN) ∈ Λ.
Зориулалт
Ламбда илэрхийллийн тэмдэглэгээг эмх замбараагүй байлгахын тулд дараах дүрмийг ихэвчлэн ашигладаг:
- Гадна хаалт орхигдсон: (MN)-ийн оронд MN.
- Хэрэглээнүүд нь холбоотой хэвээр байна гэж таамаглаж байна: ((MN) P-ийн оронд MNP гэж бичиж болно).
- Хийсвэрлэлийн бие нь цаашаа баруун тийш сунадаг: λx. MN нь λx гэсэн үг. (MN), биш (λx. M) N.
- Хийсвэрлэлийн дараалал багассан: λx.λy.λz. N нь λxyz. N байж болно.
Чөлөөт ба хязгаарлагдмал хувьсагч
Оператор λ нь хийсвэрлэлийн биеийн хаана ч байсан өөрийн тогтмол бусыг холбодог. Хамрах хүрээнд хамаарах хувьсагчдыг хязгаарлагдмал гэж нэрлэдэг. λ x илэрхийлэлд. M, λ x хэсгийг ихэвчлэн холбогч гэж нэрлэдэг. Хувьсагчдыг M дээр X x нэмснээр бүлэг болж байгааг сануулж байгаа мэт. Бусад бүх тогтворгүйг үнэгүй гэж нэрлэдэг.
Жишээ нь λ y илэрхийлэлд. x x y, y - холбоотой байнгын бус, x - чөлөөтэй. Мөн хувьсагчийг "хамгийн ойрын" хийсвэрлэлээр нь бүлэглэсэн гэдгийг тэмдэглэх нь зүйтэй. Дараах жишээнд ламбда тооцооллын шийдлийг x-ийн нэг тохиолдлоор илэрхийлсэн бөгөөд энэ нь хоёр дахь гишүүнтэй холбоотой:
λ x. у (λ x. z x)
Чөлөөт хувьсагчийн M багцыг FV (M) гэж тэмдэглэсэн бөгөөд дараах байдлаар нэр томьёоны бүтэц дээрх рекурсоор тодорхойлогддог:
- FV (x)={x}, энд x нь хувьсагч.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Чөлөөт хувьсагч агуулаагүй томьёог хаалттай гэж нэрлэдэг. Хаалттай ламбда илэрхийллүүдийг мөн нэгтгэгч гэж нэрлэдэг ба комбинатор логикийн нэр томъёотой тэнцүү байна.
Товчлол
Хамбагийн илэрхийллийн утга нь тэдгээрийг хэрхэн богиносгож чадахаар тодорхойлогддог.
Гурван төрлийн зүсэлт байдаг:
- α-хувиргах: хязгаарлагдмал хувьсагчдыг өөрчлөх (альфа).
- β-багасгах: тэдгээрийн аргументуудад функц хэрэглэх (бета).
- η-хувиргах: өргөтгөлийн тухай ойлголтыг хамарна.
Энд бас байнаБид үүссэн эквивалентуудын тухай ярьж байна: хоёр илэрхийлэл нь ижил бүрэлдэхүүн хэсэг болгон β-өөрчлөгдөж чадвал β-эквивалент бөгөөд α / η-эквивалент нь ижил төстэй байдлаар тодорхойлогддог.
Хуурч болохуйц эргэлтийн товчилсон redex гэсэн нэр томъёо нь аль нэг дүрмийн дагуу багасгаж болох дэд сэдвүүдийг хэлдэг. Даммигийн ламбда тооцоо, жишээ:
(λ x. M) N нь M дахь N-ийг х-ээр солих илэрхийлэл дэх бета редекс юм. Редексийн бууруулж буй бүрэлдэхүүн хэсгийг түүний бууралт гэнэ. Бууруулах (λ x. M) N нь M [x:=N].
Хэрвээ M-д x чөлөөтэй биш бол λ x. M x мөн зохицуулагч M-тэй em-REDEX.
α-хувиргалт
Альфа нэрийг өөрчлөх нь хязгаарлагдмал хувьсагчдын нэрийг өөрчлөх боломжийг танд олгоно. Жишээлбэл, x. x нь λ у-г өгч чадна. y. Зөвхөн альфа хувиргалтаар ялгаатай нэр томъёог α-эквивалент гэж нэрлэдэг. Ихэнхдээ ламбда тооцооллыг ашиглах үед α-эквивалентыг харилцан адилтгадаг гэж үздэг.
Альфа хөрвүүлэлтийн яг тодорхой дүрмүүд нь тийм ч энгийн зүйл биш юм. Нэгдүгээрт, энэ хийсвэрлэлээр зөвхөн ижил системтэй холбоотой хувьсагчдын нэрийг өөрчилдөг. Жишээлбэл, альфа хувиргалт λ x.λ x. x нь λ y.λ x-д хүргэж болно. x, гэхдээ энэ нь λy.λx.y-д хүргэхгүй байж магадгүй. Сүүлийнх нь анхныхаас өөр утгатай. Энэ нь хувьсах сүүдэрлэх програмчлалын үзэл баримтлалтай адил юм.
Хоёрдугаарт, альфа хувиргалт нь байнгын бус өөр хийсвэрлэлээр баригдахад хүргэж байвал боломжгүй. Жишээлбэл, хэрэв та λ x.λ y-д x-г y-ээр сольсон бол. x, тэгвэл та авч болноλy.λy. u, энэ нь огт адил биш.
Статик хамрах хүрээтэй програмчлалын хэлүүдэд нэрийн нарийвчлалыг хялбаршуулахын тулд альфа хөрвүүлэлтийг ашиглаж болно. Үүний зэрэгцээ хувьсагчийн тухай ойлголт нь агуулагдах хэсэгт тэмдэглэгээг далдлахгүй байхыг анхаарна уу.
Де Брюйн индексийн тэмдэглэгээнд альфа-тэй тэнцэх хоёр нэр томъёо синтаксийн хувьд ижил байна.
Солих
E [V:=R]-ийн бичсэн өөрчлөлтүүд нь E илэрхийлэл дэх V хувьсагчийн бүх чөлөөт тохиолдлуудыг R эргэлтээр орлуулах үйл явц юм. λ-ийн хувьд орлуулалтыг рекурсын ламбдагаар тодорхойлно. үзэл баримтлалын бүтцийн тооцооллыг дараах байдлаар хийнэ (тэмдэглэл: x ба y - зөвхөн хувьсагч, M ба N - дурын λ-илэрхийлэл).
x [x:=N] ≡ N
y [x:=N] ≡ y хэрэв 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]) хэрэв x ≠ y бол y ∉ FV (N).
Ламбда хийсвэрлэлд орлуулахын тулд заримдаа илэрхийлэлийг α-хувиргах шаардлагатай болдог. Жишээ нь, (λ x. Y) [y:=x] нь (λ x. X) үр дүнд хүрсэн нь худлаа, учир нь орлуулсан х нь чөлөөтэй байх ёстой байсан ч эцэст нь холбогддог. Энэ тохиолдолд зөв орлуулалт нь (λ z. X) α-эквивалент хүртэл байна. Орлуулах нь ламбда хүртэл өвөрмөц байдлаар тодорхойлогддог гэдгийг анхаарна уу.
β-багасгах
Бета бууралт нь функцийг ашиглах санааг илэрхийлдэг. Бета-редуктийг нэр томъёогоор тодорхойлдогорлуулах: ((X V. E) E ') нь E [V:=E'].
Жишээ нь 2, 7, × кодчилолтой гэж үзвэл дараах β-буурал гарч ирнэ: ((λ n. N × 2) 7) → 7 × 2.
Бета бууралт нь Карри-Ховард изоморфизмоор байгалийн хасалтаар орон нутгийн бууралттай байх ойлголттой ижил гэж үзэж болно.
η-хувиргах
Энэ хөрвүүлэлт нь өргөтгөлийн санааг илэрхийлдэг бөгөөд энэ утгаар хоёр функц нь бүх аргументуудад ижил үр дүнг өгөхөд тэнцүү байна гэсэн үг юм. Энэ хувиргалт нь λ x-ийн хооронд солилцдог. (F x) ба f нь f-д x чөлөөтэй биш мэт санагдах бүрт.
Энэ үйлдлийг Карри-Ховард изоморфизмоор дамжуулан байгалийн хасалт дахь орон нутгийн бүрэн байдлын үзэл баримтлалтай адил гэж үзэж болно.
Хэвийн хэлбэр ба нэгдэл
Төрөлдөөгүй ламбда тооцооллын хувьд β-багасгах дүрэм нь ерөнхийдөө хүчтэй эсвэл сул биш хэвийн байна.
Гэсэн хэдий ч α-хувиргахаас өмнө ажиллах үед β-багасалт нийлдэг болохыг харуулж байна (өөрөөр хэлбэл нэгээс нөгөөд α-хувиргах боломжтой бол хоёр хэвийн хэлбэрийг тэнцүү гэж үзэж болно).
Тиймээс хүчтэй хэвийн болгох болон сул тохируулагч нэр томъёо хоёулаа нэг хэвийн хэлбэртэй байна. Эхний нөхцлийн хувьд аливаа бууруулах стратеги нь ердийн тохиргоог бий болгох баталгаатай. Нөхцөл байдал сул байгаа бол бууруулах зарим стратеги нь үүнийг олохгүй байж магадгүй.
Програмчлалын нэмэлт аргууд
Хамбадагийн тооцоололд зориулсан олон хэлц үг бий. Тэдгээрийн олонх нь системийг програмчлалын хэлний семантикийн үндэс болгон ашиглах, доод түвшний бүтэц болгон үр дүнтэй ашиглах хүрээнд анх боловсруулагдсан. Зарим загварт ламбда тооцооллыг (эсвэл маш төстэй зүйлийг) хэсэгчилсэн байдлаар оруулдаг тул эдгээр аргууд нь практик бүтээлд бас ашиглагдах боловч ойлгомжгүй эсвэл гадаад гэж ойлгогдож болно.
Нэрлэсэн тогтмолууд
Ламбда тооцоололд номын сан нь өмнө нь тодорхойлогдсон функцуудын багц хэлбэртэй байх ба нэр томъёо нь зөвхөн тодорхой тогтмолууд юм. Бүх атомын ламбда нэр томъёо нь хувьсах хэмжигдэхүүн учраас цэвэр тооцоололд нэрлэгдсэн өөрчлөгддөггүй гэсэн ойлголт байдаггүй. Гэхдээ тэдгээрийг мөн хувиргагчийг тогтмолын нэр болгон дуурайж, бие дэх тэр дэгдэмхий бодисыг холбохын тулд lambda хийсвэрлэлийг ашиглаж, уг хийсвэрлэлийг зорьсон тодорхойлолтод хэрэглэж болно. Хэрэв та N-д М-г илэрхийлэхийн тулд f-г ашиглавалгэж хэлж болно.
(λ f. N) M.
Зохиогчид аливаа зүйлийг илүү ойлгомжтой байдлаар бичих боломжийг олгох гэх мэт синтаксийн ойлголтыг байнга нэвтрүүлдэг.
f=М-ээс N
Иймэрхүү тодорхойлолтуудыг гинжээр холбосноор нэг ламбда гишүүнээр дагаж мөрддөг тэг буюу түүнээс дээш функцын тодорхойлолтоор програмын дийлэнх хэсгийг бүрдүүлдэг эдгээр тодорхойлолтуудыг ашиглан ламбда тооцооллын "програм" бичиж болно.
Үүний анхаарал татахуйц хязгаарлалт бол f нэр нь M хэлэнд тодорхойлогдоогүй явдал юм. Учир нь M нь ламбда хийсвэрлэлийн заавал байх хүрээнээс гадуур f. Энэ нь рекурсив функцийн шинж чанарыг let-тэй M болгон ашиглах боломжгүй гэсэн үг юм. Энэ хэв маягаар рекурсив функцийн тодорхойлолт бичих боломжийг олгодог илүү дэвшилтэт letrec синтакс нь тогтмол цэгийн нэгтгэгчийг нэмэлтээр ашигладаг.
Хэвлэсэн аналогууд
Энэ төрөл нь нэргүй функцийн хийсвэрлэлийг дүрслэх тэмдэг ашигладаг шивсэн формализм юм. Энэ нөхцөлд төрөл нь ихэвчлэн ламбда нэр томъёонд хуваарилагдсан синтакс шинж чанартай объектууд юм. Тодорхой шинж чанар нь тухайн тооцоололоос хамаарна. Тодорхой өнцгөөс харахад шивсэн LI-ийг төрөлжөөгүй LI-ийн сайжруулалт гэж үзэж болно. Гэхдээ нөгөө талаас тэдгээрийг илүү суурь онол гэж үзэж болох бөгөөд төрөлжөөгүй ламбда тооцоо нь зөвхөн нэг төрлийн онцгой тохиолдол юм.
Typed LI нь програмчлалын хэлний үндэс, ML, Haskell зэрэг функциональ хэлнүүдийн үндэс юм. Мөн шууд бусаар бол бүтээлийн зайлшгүй хэв маяг. Бичсэн ламбда тооцоолол нь програмчлалын хэлний төрлийн системийг хөгжүүлэхэд чухал үүрэг гүйцэтгэдэг. Энд бичих чадвар нь ихэвчлэн програмын хүссэн шинж чанарыг агуулна, жишээлбэл, санах ойн хандалтын зөрчил үүсгэхгүй.
Бичигдсэн ламбда тоолол нь Карри-Ховард изоморфизмоор дамжуулан математик логик болон нотлох онолтой нягт холбоотой бөгөөд жишээлбэл, ангиллын ангиудын дотоод хэл гэж үзэж болно. Энэ бол зүгээр л декартын хаалтын хэв маяг юм.
