Lamda kalkülüs

Fonksiyon
x → f ( x ) {\displaystyle x\to f(x)}
Fonksiyon kavramının tarihi
Tanım ve değer kümelerine göre
X → 𝔹 𝔹 → X 𝔹n → X X → ℤ ℤ → X X → ℝ ℝ → X ℝn → X X → ℂ ℂ → X ℂn → X
Sınıflarına/özelliklerine göre
Sabit Birim Lineer Polinomyal Rasyonel Cebir Analitik Düzgün Sürekli Ölçülebilir Birebir Örten Birebir örten
Yapılarına göre
Restriction Birleşim λ Ters
Genellemelere göre
Binary relation Parçalı Çokdeğerli Implicit Space Higher-order Morphism Functor
Özel fonksiyonların listesi
g t d

Matematiksel mantıkta lamda kalkülüs (λ-kalkülüs ya da λ-calculus), fonksiyonların uygulanmasına dayanan, berimin (hesaplama) kendisini ifade etmek için kullanılan biçimsel bir sistemdir. Herhangi bir Turing makinesini çalıştırabilecek kapasiteye sahiptir. Matematikçi Alonzo Church tarafından 1930'larda matematiğin temelleri üzerine bir araştırma olarak ortaya koyulmuştur.

Lamda kalkülüs, lamda terimlerinden oluşur ve kendine has bir söz dizimi vardır. Belli dönüşüm kuralları sonucunda karmaşık değerler daha basit gösterimlere sadeleştirilebilir. BNF sözdizimi e ::= x ∣ λ x . e ∣ e e {\displaystyle e::=x\mid \lambda x{\text{.}}e\mid e\,e} şeklindedir. x , y , z {\displaystyle x,y,z} terimleri sonsuz bir isim setidir. M , N , t , s , e , f {\displaystyle M,N,t,s,e,f} terimleri ise diğer tüm lamda terimlerinin setini ifade eder. Bunun sonucunda aşağıdaki özyinelemeli tanıma varılabilir:

• x {\displaystyle x} değişkeni geçerli bir lamda terimidir
• Soyutlama, t {\displaystyle t} 'nin lamda terimi olduğu, x {\displaystyle x} 'in ise soyutlama gövdesi olduğu, ( λ x . t ) {\displaystyle (\lambda x.t)} şeklinde gösterilen bir lamda terimidir.
• Uygulama, t {\displaystyle t} ve s {\displaystyle s} 'nin diğer lamda terimleri olduğu, ( t s ) {\displaystyle (ts)} şeklinde gösterilen bir lamda terimidir.

Bir lamda terimi, bu üç kuralın tekrarlı şekilde uygulanması ile elde edilebiliyorsa söz dizimsel olarak geçerlidir. Kolaylık açısından bir lamda terimi yazılırken parantezler çoğu zaman atlanabilir.

Lamda terimleri içinde kendisini çevreleyen herhangi bir λ'nın parametresi olmayan bir değişkenin her geçtiği yer serbest olarak adlandırılır. M {\displaystyle M} teriminde x'in her serbest geçtiği yer λ x . M {\displaystyle \lambda x.M} içinde bağlıdır. M {\displaystyle M} içindeki diğer herhangi bir değişkenin serbest geçtiği yerler ise λ x . M {\displaystyle \lambda x.M} içinde serbest kalmaya devam eder.

Lamda kalkülüs Turing geçerlidir; yani herhangi bir Turing makinesini simüle etmek için kullanılabilen evrensel bir hesaplama modelidir. Adını aldığı Yunan harfi lamda (λ), lamda ifadelerinde ve lamda terimlerinde fir fonksiyondaki bir değişkenin bağlanmasını belirtmek için kullanılır.

Lamda kalkülüs tipsiz veya tipli olabilir. Tipli lamda kalkülüste fonksiyonlar yalnızca verilen girdinin "tipini" kabul edebiliyorlarsa uygulanabilirler.

Lamda kalkülüs matematik, felsefe , dilbilim ve bilgisayar bilimi gibi birçok farklı alanda uygulamaları vardır. Lamda kalkülüs programlama dili teorisinin gelişiminde önemli bir rol oynamıştır. Fonksiyonel programlama dilleri lamda kalkülüs uygular.

Lamda hesabı 1930'larda matematikçi Alonzo Church tarafından matematiğin temelleri üzerine yapılan bir araştırmanın parçası olarak ortaya atılmıştır. Orijinal sistemin, Stephen Kleene ve J.B. Rosser'ın 1935'te Kleene-Rosser paradoksunu geliştirmesiyle mantıksal olarak tutarsız olduğu gösterilmiştir.

Bunun ardından Church 1936'da yalnızca hesaplamayla ilgili kısmı ayırarak yayımlamıştır, bu kısım günümüzde tipsiz lamda kalkülüs olarak adlandırılmaktadır. 1940'ta ise hesaplama gücü daha zayıf ancak mantıksal olarak tutarlı bir sistem olan basit tipli lamda kalkülüsü de ortaya koymuştur.

Programlama dilleriyle ilişkisinin netleştiği 1960'lara kadar lamda kalkülüs yalnızca biçimsel bir sistem olarak kalmıştır. Richard Montague ve diğer dilbilimcilerin doğal dilin anlambilimdeki uygulamaları sayesinde, lamda kalkülüs hem dilbilimde hem de bilgisayar biliminde saygın bir yer edinmeye başlamıştır.

1. ^ Turing, Alan M. (December 1937). "Computability and λ-Definability". The Journal of Symbolic Logic. 2 (4): 153–163. doi:10.2307/2268280. JSTOR 2268280. 
2. ^ Coquand, Thierry (8 February 2006). Zalta, Edward N. (Ed.). "Type Theory". The Stanford Encyclopedia of Philosophy (Summer 2013 bas.). 26 Şubat 2022 tarihinde kaynağından arşivlendi. Erişim tarihi: November 17, 2020. 
3. ^ Moortgat, Michael (1988). Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus. Foris Publications. ISBN 9789067653879. 
4. ^ Bunt, Harry; Muskens, Reinhard, (Ed.) (2008). Computing Meaning. Springer. ISBN 978-1-4020-5957-5. 
5. ^ Mitchell, John C. (2003). Concepts in Programming Languages. Cambridge University Press. s. 57. ISBN 978-0-521-78098-8. .
6. ^ Chacón Sartori, Camilo (2023-12-05). Introduction to Lambda Calculus using Racket. 2023-12-07 tarihinde kaynağından arşivlendi. 
7. ^ Kleene, Stephen C.; Rosser, J. B. (July 1935). "The Inconsistency of Certain Formal Logics". The Annals of Mathematics. 36 (3): 630. doi:10.2307/1968646. JSTOR 1968646. 
8. ^ Church, Alonzo (December 1942). "Review of Haskell B. Curry, The Inconsistency of Certain Formal Logics". The Journal of Symbolic Logic. 7 (4): 170–171. doi:10.2307/2268117. JSTOR 2268117. 
9. ^ Partee, B. B. H.; ter Meulen, A.; Wall, R. E. (1990). Mathematical Methods in Linguistics. Springer. ISBN 9789027722454. Erişim tarihi: 29 Dec 2016. 
10. ^ Alama, Jesse. Zalta, Edward N. (Ed.). "The Lambda Calculus". The Stanford Encyclopedia of Philosophy (Summer 2013 bas.). 26 Şubat 2022 tarihinde kaynağından arşivlendi. Erişim tarihi: November 17, 2020. 

Matematik ile ilgili bu madde taslak seviyesindedir. Madde içeriğini genişleterek Vikipedi'ye katkı sağlayabilirsiniz.