Lambda Kalkülü ve Fonksiyonel Modeller
Lambda kalkülü, her şeyin bir fonksiyon olduğu ve hesaplamanın yerine koyma (substitution) yoluyla ilerlediği minimal bir biçimsel sistemdir; bu sistem hem etkili hesaplamanın erken bir modelini hem de fonksiyonel programlamanın teorik çekirdeğini sağlamaktadır.
Tanım
Lambda kalkülü, değişkenlerden, fonksiyon soyutlamasından ve uygulamadan oluşan biçimsel bir dildir; hesaplama, bir fonksiyonu bir argümana yerine koyma yoluyla uygulayan beta indirgeme (beta reduction) kuralı ile gerçekleştirilmektedir; bu, Turing makineleriyle güç açısından eşdeğer evrensel bir modeldir.
Kapsam
Bu konu, lambda terimlerinin sözdizimini, hesaplamayı yönlendiren indirgeme kurallarını, Church–Rosser birleşme özelliğini, sabit nokta kombinatörleri aracılığıyla veri ve özyinelemenin kodlanmasını, kalkülüsün Turing-tamlığını ve hesaplamayı mantıkla ilişkilendiren tipli varyantlarını kapsamaktadır.
Temel sorular
- Hesaplama, yalnızca fonksiyonlar ve yerine koyma kullanılarak nasıl ifade edilebilir?
- İndirgeme sırası neden nihai sonucu değiştirmez?
- Sayılar, veriler ve özyineleme tamamen fonksiyonlarla nasıl temsil edilir?
- Tipli lambda kalkülüsleri hesaplamayı mantıksal kanıtla nasıl ilişkilendirir?
Temel kuramlar
- Church–Rosser teoremi
- Bir lambda terimi farklı şekillerde indirgenebilirse, sonuçlar her zaman bir araya getirilebilir; bu nedenle her terimin en fazla bir normal formu vardır ve kalkülüs, bir hesaplama modeli olarak birleşiktir ve iyi tanımlanmıştır.
- Turing-tamlığı ve sabit noktalar
- Sabit nokta kombinatörleri keyfi özyinelemeyi ifade ederek, tiplendirilmemiş lambda kalkülüsünü her Turing-hesaplanabilir fonksiyonu hesaplayabilir hale getirmekte ve böylece tam bir hesaplama modeli sunmaktadır.
- Curry–Howard yazışması
- Tipli lambda kalkülüsleri, önermeler olarak tipler ve kanıtlar olarak programlar ile mantık sistemlerine karşılık gelmekte, hesaplamayı doğrudan yapıcı mantıkla ilişkilendirmekte ve kanıt asistanlarının temelini oluşturmaktadır.
Klinik önem
Lambda kalkülü, Lisp, Haskell ve ML gibi fonksiyonel programlama dillerinin, modern dillerdeki hataları yakalayan tip sistemlerinin ve Curry–Howard yazışmasının programlar ile matematiksel kanıtların aynı mekanizma tarafından kontrol edilmesini sağladığı kanıt asistanlarının temelini oluşturmaktadır.
Tarihçe
Church, 1930'larda lambda kalkülüsünü mantık ve hesaplama için bir temel olarak tanıtmış ve Rosser ile birlikte onun birleşmesini kanıtlamıştır. Orijinal mantıksal sistem tutarsız olmasına rağmen, hesaplama çekirdeği gelişmiş ve 1960'lardan itibaren fonksiyonel programlamayı ve Curry–Howard yazışması aracılığıyla kanıtlar ile programlar arasındaki bağlantıyı şekillendirmiştir.
Öne çıkan isimler
- Alonzo Church
- Haskell Curry
- J. Barkley Rosser
- William Alvin Howard
İlgili konular
Temel eserler
- church1936
- barendregt1984
Sıkça sorulan sorular
- Sadece fonksiyonları olan bir sistem sayılarla nasıl hesaplama yapabilir?
- Sayılar fonksiyonlar olarak kodlanmaktadır; örneğin, Church sayıları, belirli bir işlemin kaç kez uygulandığına göre bir sayıyı temsil etmektedir. Aritmetik, boole değerleri, çiftler ve veri yapıları, hepsi fonksiyonel kodlamalara sahiptir, bu nedenle kalkülüsün yerleşik veri tiplerine ihtiyacı olmamasına rağmen her türlü hesaplamayı ifade edebilmektedir.
- Lambda kalkülü ile programlama arasındaki bağlantı nedir?
- Fonksiyonel diller esasen genişletilmiş lambda kalkülüsleridir: çekirdekleri fonksiyonlar, uygulama ve yerine koymadır. Kalkülüs ayrıca modern dillerin güvenlik için kullandığı tip teorisini sağlamakta ve Curry–Howard yazışması aracılığıyla iyi tiplendirilmiş programları mantıksal kanıtlarla ilişkilendirmektedir.