Saf lambda analizinde sıralama veya devamlılık geçişi
Burada verilen aşağıdaki alıştırmayı çözmeye çalışıyorum .
Aşağıdaki sayı temsilini düşünün. Ekleme nasıl tanımlanır?
|0| = λx.x
|1| = λx.λx.x
...
|n + 1| = λx.|n|
Halef ve önceki operatörlerin tanımlanması kolaydır:
Succ n = λx.n
Pred n = n (λx.x)
Toplamayı tanımlamak için "açık" bir çözüm, ardıl işlem artı sıfır için testin sabit nokta birleştirici ile birlikte kullanılmasıdır, aşağıda verilen F için (YF) gibi bir şey ( if ve booleler her zamanki gibi tanımlanmıştır):
F = λf.(λm n. if (Is0 m) n (Succ (f (Pred m) n))
Ancak Is0'ı tanımlamak önemsiz görünmüyor. Sorun şu ki bir | N | N + 1 argüman tüketir ve N argüman basitçe onun tarafından silinir. Bu nedenle, eğer böyle bir işlevi uygularsam, rakamın, örneğin bir kimlik olmadığı netleştiğinde, uygulamasını durdurmak makul görünür. Sanırım bu bir çeşit devam, ama onu saf lambda-kalkülüsünde nasıl modelleyeceğimi hayal edemiyorum. Belki birisi yardımcı olabilecek herhangi bir ipucu biliyordur?
Bir sıralama operatörü de eklemeyi tanımlamaya yardımcı olabilir. Bir sayı uygulaması ise | m | bir sayıya kadar ertelenir | n | tüm bağımsız değişkenlerine uygulanırsa , sonuç tam olarak bir sayı olacaktır | n + m | . Belki de saf lambda-kalkülüsünde böyle bir sıralama birleştiricisinin bir çeşidi vardır?
Alıştırmanın yazarı tarafından verilen cevap saf olmayan bir işlem kullanır (yani, argümanının bir işlev olup olmadığını kontrol eden IsProcedure ).
UPD: Lambda-hesaplamada CPS yapmak zor değildir (CBV ile ilgili ayrıntılar burada bulunabilir ). Görünüşe göre bu sorunu çözmek için yeterli değil.
UPD : Saf lambda-hesabı için bir çeşit quote-eval fonksiyonlarına sahipsek, o zaman bir fonksiyon olmalı$eq$, bu, alıntılanan lambda ifadelerinin sözdizimsel olarak eşit olup olmadığını tanır ve Is0'ı kullanarak$eq$. Ama bundan şüpheliyim$eq$tanımlanabilir. Nedeni "genellik lemması" dır (Barendregt kitabı, lemma 14.3.24). Eşitliği alıntılanan lambda terimlerinde test edebilseydik ($eq$( Alıntı $\Omega$) ( Alıntı $\lambda x.x$)) dönecekti $False$ve genellik şunu ima eder ($eq$( Alıntı $\lambda x.x$) ( Alıntı $\lambda x.x$)) ayrıca geri döner $False$. Bu , saf lambda-kalkülüsünde Alıntı oluşturma olasılığıyla çelişiyor mu ?
Yanıtlar
Saf lambda hesabında aradığınızı bulacağınızı sanmıyorum. Anahtar, yaptığınız şu ifadedir:
Bir sıralama operatörü de eklemeyi tanımlamaya yardımcı olabilir. Bir sayı uygulaması ise | m | bir sayıya kadar ertelenir | n | tüm argümanlarına uygulanır, ...
Lambda hesabının modellerinin şöyle olması gerekiyordu:
$$U \cong U^U$$
Ve bunun amacı, her anlamsal değerin$u \in U$bir şeye uygulanabilir. Dolayısıyla, "tüm argümanlarına uygulanan" bir şeyden bahsetmenin bir anlamı yoktur. Saf lambda hesabında daha fazla argümana uygulanamayacak bir değer yoktur.
IsZeroBazılarının düşünmesi olası görünmese de , doğalların bu temsilinin uygulamayı imkansız kıldığına dair bir model / argüman elinden bilmiyorum . Bununla birlikte, saf lambda hesabında mümkün olacaksa, anlamsal olarak anlam ifade etmesi ve sadece sözdizimsel olan kavramlara dayanmaması gerekecektir.
Düzenleme: İşte bir argümanın bir taslağı. Bir tanımı$\mathsf{IsZero}$ sonunda aşağıdaki gibi azaltılmalıdır:
$$\mathsf{IsZero}\ n \rightsquigarrow^* n \overrightarrow v$$
Bunun nedeni, lambda hesaplamasında sayıları gerçekten ayırt etmek için belirli sayıda değere uygulamanın tek mekanizma olmasıdır. Durum böyle olmalıdır:$$0 \overrightarrow v = \mathsf{true} \\ \mathsf{s}n \overrightarrow v = \mathsf{false}$$ Ancak her biri için $\overrightarrow v$ durum şu: $$||\overrightarrow v| + k|\overrightarrow v = |k|$$ (nerede $|\overrightarrow v|$ uzunluğu $\overrightarrow v$). Ama yalnızca$|1| = \mathsf{false}$(eğer seçilen kural buysa). İngilizcede, bir rakam uygulayarak bir boole elde etmek için gereken terimlerin sayısı konusunda bir sınır yoktur. Yani olamaz$\overrightarrow v$ tüm sayılar için denklemleri sağlayan ve dolayısıyla $\mathsf{IsZero}$ tanımlanamaz.