şükela:  tümü | bugün
  • (bkz: scheme)
    (bkz: lisp)
  • t -> v (degiskene deger ata)
    t -> (lambda v t) (fonksiyon tanimla)
    t -> (t t) (fonksiyon cagir)

    seklinde ozetlenebilecek matematiksel sistem. tum sozdizimi bundan ibarettir. semantigi ise biraz daha uzundur (4-5 formul falan). computation theory anlaminda turing makinasina denk bir modeldir.

    (bkz: beta reduction)
  • gerekli malzemeler:
    1.variable
    2.function
    3.function application
  • (bkz: alpha conversion)
    (bkz: beta reduction)
    (bkz: eta conversion)
    ve son olarak (bkz: redex)
  • alonso church tarafından ortaya atılmıştır.

    lambda calculus ile ilgili en kaydadeğer* nokta şudur:

    alan turing, bir makine ve bir teyp (ikisinin toplamı: turing machine)'i kullanarak neyin hesaplanabilir * olup neyin hesaplanamaz olduğunu açıklayan ilk adamdır.
    o zamana kadar, bu turing makinesinin öncesinde, turing makinesi kadar esnekliği/hesaplama kabiliyeti olmayan türde automaton'lar üzerine de çalışılmıştır.

    örneğin deterministic finite automaton'lar vardır, a^(n).b^(n) şeklinde bir inputu kabul edecek bir deterministic finite automaton bulamazsınız. o iş dfa'ler için hesaplanabilir değildir.
    örneğin pushdown automata vardır, biraz önceki söylediğimi bulur; fakat a^(n).b^(2n).c^(n) şeklindeki bir inputu kabul edemez.
    bu arada, bu iki örnekte bahsettiğim başarısız olma durumları pumping lemma denilen bir lemma ile kanıtlanabilir.

    tabii bunlardan sonra alan turing'in çıkıp 'bu makine hesaplanabilen her şeyi hesaplar' *demesiyle yer yerinden oynuyor. burada bahsettiği 'hesaplanabilen' tanımı, bu makineye bağımlı bir tanım oluyor.

    fakat alonso church, lambda calculus'u ile sahneye çıktığında, ortada artık bir makine falan yok. church, alan turing'in hesaplanabilir dediği şeyleri birebir açıklayan, ve bunu sadece soyut matematik kullanarak yapan bir mekanizma icat ediyor aslında.

    computability (hesaplanabilirlik) konseptini 'bir makinenin çalışmasından meydana gelen bir süreç' olmaktan çıkarıyor church. işte bu yüzden çok önemlidir lambda calculus.
  • (bkz: alan turing)'in doktora supervisoru olan (bkz: alonso church)'ün "hesaplanabilirlik bakış açısıyla bakıldığında işlev kavramı nasıl olmalıdır?" sorusuna verdiği fonksiyonel tabanlı cevaptır "lambda calculus". turing makineleri de aynı soruya durum tabanlı bir çözüm getirdiğinden, sıklıkla beraber anılırlar. (bkz: chuch-turing hipotezi).

    church'e göre bir fonksiyon, içine bakmamanız gereken bir kara kutudur. bu fonksiyon bazı girdiler alır, bunları bir şekilde işler ve bir çıktı üretir. fonksiyonun işleme mantığı önemli değildir ancak "pure" olmaları şarttır. yani: girdiler harici bir parametreye (duruma) bağlı olarak ürettikleri sonuç değişmez ve yan etki de üretmezler. bu açıdan bakıldığında durum tabanlı turing makineleri ile taban tabana zıttır denebilir.

    lx. x+1
    lx.ly x+y

    şeklinde yazılırlar.

    bu notasyon kullanarak sıralı satırların işlenmesi rutini ile çalışan veya gelecekte çalışacak herhangi bir program kodlanabilir (aynı turing makinelerinde olduğu gibi).

    bu bilgilere dayanarak, turing makineleri ile kodlanabilen herhangi bir programın lambda calculus ile; lambda notasyonu ile kodlanabilen her programın turing makineleri ile kodlanabileceğini söyleyebiliriz.

    ml ailesi ve haskell gibi fonksiyonel programlama dillerinin temelinde lambda calculus yatar. son beş on yıldır bilinen bir çok oop programa dili de lambda calculus'u temel özellik olarak sunmaktadır.
  • her şeyin fonksiyon olduğu bir matematik sistemi. sayıların ve booleanların gösterimleri için bile fonksiyonlar kullanılır. örnek vermek gerekirse genel olarak booleanlar:

    true = /x. /y. x
    false=/x. /y. y
    (/ işaretleri lambda sembolü olacak)

    olarak gösterilebilir. aslında bu iki fonksiyon her ne kadar da gerçekten doğru veya yanlışın karşılığı olmasa da seçim yapabilmek için bir mekanizma oluştururlar, true ilk argümanına indirgenirken false ise ikinci argümanına indirgenir. bu şekilde lojik devrelerin elemanlarının çalışma mantıkları da taklit edilebilir, örnek vermek gerekirse:

    not = /x. x false true

    fonksiyonu için eğer x için false verirseniz beta reduction ile

    false false true

    fonksiyonuna indirgenir. en soldaki false ikinci argümana indirgeneceği için sonuç true olur. aynısı true false true için de false’tur. and devresi için ise:

    and = /x. /y. xyx

    kullanılabilir. bu fonksiyonda ise eğer x true ise y’nin değerine indirgenir ve eğer y true ise sonuç true olur değilse olmaz. eğer x false ise x’e indirgenir ve otomatik olarak sonuç false’a indirgenir. not ve and kullanılarak aşağıdaki şekilde nand yapılabileceği için de oradan tüm devreleri oluşturabiliriz çünkü nand devresi turing completedir.

    nand = /x. /y. not ( and x y )

    bunun yanında sayıların gösterimi için ise kullanılan notasyon aşağıdaki şekildedir:

    0 = /f. /x. x (dikkat ettiyseniz false ile aynı fonksiyon)
    1 = /f. /x. f x
    2 = /f. /x. f (f x)
    3 = /f. /x. f ( f (f x))
    ...

    bu notasyon ise sayının argüman olarak aldığı x’in argüman olarak aldığı f’e kendi değeri kadar uygulanmasını sağlar.aritmetik işlemlerinden en basit olanı bir arttırma işlemidir ve şu şekilde gösterilebilir:

    incr = /n. /f. /x. f (n f x)

    bunu test etmek için bir değeriyle denersek:

    (/n. /f. /x. f (n f x)) ( /f. /x. f x) =
    /f. /x. f ( (/g. /y. g y )f x) =
    /f. /x. f(f(x))

    şeklinde iki değerini elde ederiz. bu fonksiyondan ve önce bahsettiğimiz kendi değeri kadar argüman aldığı fonksiyonu argüman aldığı diğer fonksiyona uygulayabilmesi özelliğiyle birlikte toplama işlemini:

    add = /n. /m. n incr m

    yada indirgenmiş haliyle:

    add = /n. /m. /f. /x. n f ( m f x )

    olarak yazabiliriz. çıkarma işlemi için ise bir eksiltme operatörünü tanımlayabilmemiz gerekir. bu işlem arttırma kadar kolay bir işlem değildir çünkü zaten uygulanmış bir fonksiyonu direk olarak geri alamayız. bu işlemi yapmanın bir yolu azaltacağımız sayıya kadar bir sayıyı teker teker arttırıp bir kademe önceki sayıyı almaktır.bunun için önce sayı çiftinin tanımını yapmamız gerekir:

    pair = /x. /y. /f. f x y

    şeklinde tanımlanabilir.

    pair 2 3

    dendiğinde bu pair fonksiyonuna x ve y değerleri olarak 2 ve 3 verir ve geriye:

    /f. 2 3

    kalır ki bu durumun adı partial applicationdur ve çoğu fonksiyonel dilde bulunan bir özelliktir. son olarak da bu sayı çiftinin değerlerinden birini alabilmek için bu fonksiyona en tepedeki true veya false değerini vermek yeter.

    bu işlemin çıkarma işlemi için olan önemi ise bizim bu sayı çiftinin sürekli olarak birinci değerini ikinci değerine eşitleyip ikinci değerini bir arttırarak bir azaltacağımız sayının bir azını bulacak olmamızdır, bu işlemin bir iterasyonu şu şekilde tanımlanabilir:

    iterate = /p. pair ( p false) (incr (p false))

    ve bu şekilde bir azı bulma fonksiyonu da:

    decr= /n. (n iterate pair (0 0)) true

    olarak tanımlanabilir ve çıkartma işlemi:

    sub = /n. /m. m decr n

    olarak tanımlanabilir.