Lambda hesabı, soyutlamaya dayalı hesaplamaları ifade etmek ve bağlama ve değişken ikamesi kullanarak işlevleri uygulamak için matematiksel mantıkta resmi bir sistemdir. Bu, herhangi bir Turing makinesinin tasarımına uygulanabilecek evrensel bir modeldir. Lambda hesabı ilk olarak 1930'larda ünlü bir matematikçi olan Church tarafından tanıtıldı.
Sistem, lambda elemanlarının oluşturulması ve üzerlerinde indirgeme işlemlerinin yapılmasından oluşur.
Açıklamalar ve Uygulamalar
Yunanca lambda (λ) harfi lambda ifadelerinde ve bir fonksiyondaki bir değişkenin bağlanmasını belirtmek için lambda terimlerinde kullanılır.
Lambda hesabı türlenmemiş veya yazılabilir. İlk varyantta, işlevler yalnızca bu türden verileri alabiliyorlarsa kullanılabilir. Yazılan lambda taşları daha zayıftır, daha küçük bir değer ifade edebilir. Ama öte yandan, daha fazla şey kanıtlamanıza izin veriyorlar.
Bu kadar çok farklı türün olmasının bir nedeni, bilim adamlarının güçlü lambda hesabı teoremlerini kanıtlama fırsatından vazgeçmeden daha fazlasını yapma arzusudur.
Sistemin matematik, felsefe, dilbilim ve bilgisayar biliminin birçok farklı alanında uygulamaları vardır. Öncelikle lambda hesabı, programlama dilleri teorisinin gelişmesinde önemli rol oynamış bir hesaptır. Sistemlerin uyguladığı işlevsel yaratma stilleridir. Ayrıca, bu kategorilerin teorisinde sıcak bir araştırma konusudur.
Aptallar için
Lambda hesabı, 1930'larda matematikçi Alonzo Church tarafından bilimin temelleri üzerine yaptığı araştırmanın bir parçası olarak tanıtıldı. 1935'te Stephen Kleen ve J. B. Rosser, Kleene-Rosser paradoksunu geliştirdiğinde, orijinal sistemin mantıksal olarak tutarsız olduğu gösterildi.
Daha sonra, 1936'da Church, yalnızca hesaplamalarla ilgili olan kısmı seçti ve yayınladı, bu kısım şimdi yazılmamış lambda hesabı olarak adlandırılıyor. 1940'ta ayrıca asal tip sistem olarak bilinen daha zayıf ama mantıksal olarak tutarlı bir teori ortaya koydu. Çalışmasında tüm teoriyi basit terimlerle açıklıyor, bu nedenle Church'ün aptallar için calculus lambda yayınladığı söylenebilir.
Programlama dilleriyle ilişkisinin netleştiği 1960'lara kadar λ sadece bir formalizmdi. Richard Montagu ve diğer dilbilimcilerin doğal dilin semantiğindeki uygulamaları sayesinde, kalkülüs hem dilbilim hem de bilgisayar bilimlerinde yerini aldı.
Sembolün kökeni
Lambda bir kelimenin veya kıs altmanın yerine geçmez, Russell'ın Temel Matematiğindeki bir referanstan ve ardından iki tipografik değişiklikten gelir. Notasyon örneği: f (y)=2y + 1 olan bir f fonksiyonu için 2ŷ + 1'dir. Ve burada giriş değişkenini etiketlemek için y üzerinde bir şapka (“şapka”) kullanıyoruz.
Kilise başlangıçta benzer semboller kullanmayı amaçlamıştı, ancak dizgiciler "şapka" sembolünü harflerin üzerine yerleştiremediler. Bunun yerine orijinal olarak "/\y.2y+1" olarak yazdırdılar. Bir sonraki düzenleme bölümünde, daktilo yazarları "/ \" yerine görsel olarak benzer bir karakter koydu.
Lambda kalkülüsüne giriş
Sistem, belirli bir biçimsel sözdizimi tarafından seçilen bir terimler dilinden ve bunların manipüle edilmesine izin veren bir dizi dönüştürme kuralından oluşur. Son nokta, bir denklem teorisi veya işlemsel bir tanım olarak düşünülebilir.
Lambda hesabındaki tüm işlevler anonimdir, yani adları yoktur. Yalnızca bir girdi değişkeni alırlar ve körleme, birden çok değişkenli grafikleri uygulamak için kullanılır.
Lambda terimleri
Hesap sözdizimi, bazı ifadeleri geçerli ve diğerlerini geçersiz olarak tanımlar. Tıpkı farklı karakter dizilerinin geçerli C programları olduğu ve bazılarının geçerli olmadığı gibi. Lambda hesabının gerçek ifadesine "lambda terimi" denir.
Aşağıdaki üç kural, endüktif bir tanım sağlar.tüm sözdizimsel olarak geçerli kavramların oluşturulmasına uygulanır:
x değişkeninin kendisi geçerli bir lambda terimidir:
- T LT ise ve x sabit değilse, o zaman (lambda xt) bir soyutlama olarak adlandırılır.
- Eğer T ve s kavramlar ise, o zaman (TS) bir uygulama olarak adlandırılır.
Başka hiçbir şey lambda terimi değildir. Dolayısıyla bir kavram ancak ve ancak bu üç kuralın tekrar tekrar uygulanmasıyla elde edilebiliyorsa geçerlidir. Ancak bazı parantezler diğer kriterlere göre atlanabilir.
Tanım
Lambda ifadeleri şunlardan oluşur:
- değişkenler v 1, v 2, …, v n, …
- soyutlama sembolleri 'λ' ve nokta '.'
- parantez ().
set kümesi tümevarımsal olarak tanımlanabilir:
- x bir değişkense, x ∈ Λ;
- x sabit değildir ve M ∈ Λ, o zaman (λx. M) ∈ Λ;
- M, N ∈ Λ, sonra (MN) ∈ Λ.
Tanım
Lambda ifadelerinin gösterimini düzenli tutmak için aşağıdaki kurallar yaygın olarak kullanılır:
- Dış parantezler atlandı: (MN) yerine MN.
- Uygulamaların ilişkisel kaldığı varsayılır: ((MN) P yerine MNP yazılabilir).
- Soyutlamanın gövdesi daha sağa doğru uzanır: λx. MN, λx anlamına gelir. (MN), değil (λx. M) N.
- Soyutlamaların sırası az altılır: λx.λy.λz. N, λxyz. N. olabilir
Serbest ve bağlı değişkenler
İşleci λ, sabit olmayanını soyutlama gövdesinin neresinde olursa olsun birleştirir. Kapsama giren değişkenlere bağlı denir. λ x ifadesinde. M, λ x kısmı genellikle bağlayıcı olarak adlandırılır. Sanki X x'in M'ye eklenmesiyle değişkenlerin bir grup haline geldiğini ima ediyormuş gibi. Diğer tüm kararsızlara serbest denir.
Örneğin, λ y ifadesinde. x x y, y - kalıcı olmayan bağlı ve x - serbest. Ayrıca değişkenin "en yakın" soyutlamasına göre gruplandırıldığını da belirtmekte fayda var. Aşağıdaki örnekte, lambda hesabı çözümü, ikinci terimle ilgili tek bir x oluşumuyla temsil edilir:
λ x. y (λ x. z x)
M serbest değişkenler kümesi FV (M) olarak gösterilir ve aşağıdaki gibi terimlerin yapısı üzerinde yineleme ile tanımlanır:
- FV (x)={x}, burada x bir değişkendir.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Serbest değişkenler içermeyen formüle kapalı denir. Kapalı lambda ifadeleri birleştirici olarak da bilinir ve birleşimsel mantıktaki terimlere eşdeğerdir.
Kıs altma
Lambda ifadelerinin anlamı, nasıl kıs altılabileceğine göre belirlenir.
Üç tür kesim vardır:
- α-dönüşüm: bağlı değişkenleri değiştirme (alfa).
- β-indirgeme: işlevleri bağımsız değişkenlerine uygulama (beta).
- η-dönüşüm: genişleme kavramını kapsar.
İşte burada dasonuçta ortaya çıkan eşdeğerliklerden bahsediyoruz: iki ifade aynı bileşene β-dönüştürülebiliyorsa β-eşdeğerdir ve α / η-eşdeğerliği benzer şekilde tanımlanır.
İndirgenebilir cironun kıs altması olan redex terimi, kurallardan biri tarafından az altılabilen alt konuları ifade eder. Aptallar için lambda hesabı, örnekler:
(λ x. M) N, M'de N'yi x ile değiştirme ifadesinde bir beta redex'tir. Redex'in indirgendiği bileşene onun indirgenmesi denir. İndirgeme (λ x. M) N, M [x:=N]'dir.
Eğer x M'de serbest değilse, λ x. M x ayrıca M. regülatörlü em-REDEX
α-dönüşüm
Alfa yeniden adlandırmaları, bağlı değişkenlerin adlarını değiştirmenize olanak tanır. Örneğin, x. x, λ y'yi verebilir. y. Yalnızca alfa dönüşümünde farklılık gösteren terimlere α eşdeğeri denir. Genellikle, lambda hesabı kullanılırken, α-eşdeğerleri karşılıklı olarak kabul edilir.
Alfa dönüştürme için kesin kurallar tamamen önemsiz değildir. İlk olarak, bu soyutlama ile yalnızca aynı sistemle ilişkili değişkenler yeniden adlandırılır. Örneğin, alfa dönüşümü λ x.λ x. x, λ y.λ x'e yol açabilir. x, ancak bu λy.λx.y'ye yol açmayabilir. İkincisi orijinalinden farklı bir anlama sahiptir. Bu, değişken gölgeleme programlama kavramına benzer.
İkincisi, kalıcı olmayan başka bir soyutlama tarafından yakalanmasıyla sonuçlanacaksa bir alfa dönüşümü mümkün değildir. Örneğin, λ x.λ y'de x'i y ile değiştirirseniz. x, o zaman alabilirsinλy.λy. u, ki bu hiç de aynı değil.
Statik kapsamı olan programlama dillerinde, ad çözümlemesini basitleştirmek için alfa dönüştürme kullanılabilir. Aynı zamanda, değişken kavramının içerdiği alandaki atamayı maskelememesine dikkat etmek.
De Bruyne dizin gösteriminde, herhangi iki alfa eşdeğeri terim sözdizimsel olarak aynıdır.
Değiştirme
E [V:=R] tarafından yazılan değişiklikler, E ifadesindeki V değişkeninin tüm serbest oluşumlarını R cirosu ile değiştirme işlemidir. λ cinsinden değiştirme, özyinelemenin lambdası ile tanımlanır. kavram yapısı üzerinde aşağıdaki gibi hesap yapın (not: x ve y - yalnızca değişkenler ve M ve N - herhangi bir λ ifadesi).
x [x:=N] ≡ N
y [x:=N] ≡ y eğer 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 ise, y ∉ FV (N) olması şartıyla.
Lambda soyutlamasına ikame yapmak için bazen bir ifadeyi α-dönüştürmek gerekir. Örneğin, (λ x. Y) [y:=x]'in (λ x. X) ile sonuçlanması doğru değildir, çünkü ikame edilen x'in serbest olması gerekirdi, ancak sonunda bağlıydı. Bu durumda doğru yer değiştirme (λ z. X) α-eşdeğerliğine kadardır. Değiştirmenin lambda'ya kadar benzersiz şekilde tanımlandığını unutmayın.
β-indirgeme
Beta az altma, bir işlev uygulama fikrini yansıtır. Beta indirgeyici terimlerle tanımlanırikame: ((X V. E) E ') E [V:=E']'dir.
Örneğin, 2, 7, × kodlamasını varsayarsak, şu β-indirgenmesi vardır: ((λ n. N × 2) 7) → 7 × 2.
Beta indirgemesi, Curry-Howard izomorfizmi aracılığıyla doğal kesinti altında yerel indirgenebilirlik kavramıyla aynı şey olarak görülebilir.
η-dönüşüm
Bu dönüşüm, bu bağlamda tüm argümanlar için aynı sonucu verdiklerinde iki fonksiyonun eşit olduğu genişletilebilirlik fikrini ifade eder. Bu dönüşüm λ x arasında değişir. (F x) ve f, f'de x özgür görünmediğinde.
Bu eylem, Curry-Howard izomorfizmi aracılığıyla doğal tümdengelimdeki yerel tamlık kavramıyla aynı olarak düşünülebilir.
Normal formlar ve füzyon
Türlenmemiş bir lambda hesabı için, β-indirgeme kuralı genellikle ne güçlü ne de zayıf normalleştirmedir.
Yine de, β-redüksiyonunun α-dönüşümünden önce çalıştırıldığında birleştiği gösterilebilir (yani, birinden diğerine bir α-dönüşümünün mümkün olması durumunda iki normal form eşit kabul edilebilir).
Bu nedenle, hem güçlü normalleştirici terimler hem de zayıf ayarlı terimler tek bir normal forma sahiptir. İlk terimler için, herhangi bir az altma stratejisinin tipik bir konfigürasyonla sonuçlanması garanti edilir. Zayıf normalleştirme koşulları için, bazı az altma stratejileri onu bulamayabilir.
Ek programlama yöntemleri
Lambda hesabı için bir çok yaratılış deyimi vardır. Birçoğu, başlangıçta, sistemlerin bir programlama dilinin semantiğinin temeli olarak kullanılması bağlamında geliştirildi ve bunları düşük seviyeli bir yapı olarak etkin bir şekilde uyguladı. Bazı stiller, bir snippet olarak bir lambda hesabı (veya çok benzer bir şey) içerdiğinden, bu teknikler pratik yaratmada da kullanım bulur, ancak daha sonra belirsiz veya yabancı olarak algılanabilir.
Adlandırılmış sabitler
Lambda hesabında, bir kitaplık, terimlerin yalnızca somut sabitler olduğu, önceden tanımlanmış bir dizi fonksiyon şeklini alır. Tüm atomik lambda terimleri değişken olduğundan, saf hesabın adlandırılmış değişmezler kavramı yoktur. Ancak, değişkeni sabitin adı olarak alarak, vücuttaki uçucuyu bağlamak için bir lambda soyutlaması kullanarak ve bu soyutlamayı amaçlanan tanıma uygulayarak da taklit edilebilirler. Yani, N'deki M'yi temsil etmek için f kullanırsanız,diyebilirsiniz.
(λ f. N) M.
Yazarlar genellikle bir şeylerin daha sezgisel bir şekilde yazılmasına izin vermek gibi sözdizimsel bir kavram sunar.
f=M'den N'ye
Bu tür tanımları zincirleyerek, programın büyük kısmını oluşturan bu tanımları kullanarak, sıfır veya daha fazla fonksiyon tanımı ve ardından tek bir lambda üyesi olarak bir lambda hesabı "programı" yazılabilir.
Bu letin dikkate değer bir sınırlaması, f adının M'de tanımlı olmamasıdır,M, lambda soyutlamasının bağlayıcı kapsamı dışında olduğundan f. Bu, özyinelemeli bir işlev özniteliğinin let ile M olarak kullanılamayacağı anlamına gelir. Bu tarzda özyinelemeli işlev tanımları yazmanıza izin veren daha gelişmiş letrec sözdizimi, bunun yerine ek olarak sabit nokta birleştiricileri kullanır.
Basılı analoglar
Bu tür, anonim bir işlev soyutlamasını temsil etmek için bir sembol kullanan yazılı bir biçimciliktir. Bu bağlamda, türler genellikle lambda terimlerine atanan sözdizimsel nitelikteki nesnelerdir. Kesin doğası, söz konusu hesaba bağlıdır. Belirli bir bakış açısından, yazılan LI, yazılmamış LI'nin iyileştirmeleri olarak düşünülebilir. Ancak öte yandan, daha temel bir teori olarak da kabul edilebilirler ve türlenmemiş lambda hesabı, yalnızca bir türe sahip özel bir durumdur.
Yazılan LI, programlama dillerinin temeli ve ML ve Haskell gibi işlevsel dillerin omurgasıdır. Ve daha dolaylı olarak, zorunlu yaratma tarzları. Yazılan lambda hesapları, programlama dilleri için tip sistemlerinin geliştirilmesinde önemli bir rol oynamaktadır. Burada yazılabilirlik genellikle programın istenen özelliklerini yakalar, örneğin bir bellek erişim ihlaline neden olmaz.
Türlü lambda hesapları, Curry-Howard izomorfizmi aracılığıyla matematiksel mantık ve ispat teorisi ile yakından ilişkilidir ve kategori sınıflarının dahili bir dili olarak düşünülebilir.basitçe Kartezyen kapanışların tarzıdır.
