S ^m _n teorem - S^m_n theorem

Gelen Hesaplama teorisi S   m
n   teoremi (ayrıca adlandırılan çeviri lemma , teoremi parametre ve ölçülebilirliği teoremi ) hakkında temel bir sonuçtur programlama dilleri (daha genel olarak ve Gödel numberings ait hesaplanabilir fonksiyonlar ) (Soare 1987, Rogers 1967). İlk olarak Stephen Cole Kleene (1943) tarafından kanıtlandı . Adı S   m
n   teoremin orijinal formülasyonunda alt simge n ve üst simge m olan bir S'nin oluşumundan gelir (aşağıya bakınız).

Pratik terimlerle teorem, belirli bir programlama dili ve pozitif tamsayılar m ve n için , m  +  n serbest değişkenli bir programın kaynak kodunu , m değerleriyle birlikte girdi olarak kabul eden belirli bir algoritma olduğunu söyler . Bu algoritma, ilk m serbest değişkenlerinin değerlerini etkin bir şekilde ikame eden ve değişkenlerin geri kalanını serbest bırakan kaynak kodu üretir .

Detaylar

Teoremin temel formu iki argümanın fonksiyonları için geçerlidir (Nies 2009, s. 6). Bir Gödel'in numaralandırma verilen yinelemeli fonksiyonları, bir olduğu ilkel özyinelemeli fonksiyon s , aşağıdaki özellikleri olan iki bağımsız değişken: Her Gödel'in sayısı için p kısmi hesaplanabilir fonksiyonu f iki bağımsız, ifadeler ile ve doğal sayılar aynı kombinasyonları için tanımlandığı gibidir x ve y ve değerleri böyle herhangi bir kombinasyon için eşittir. Diğer bir deyişle, her x için aşağıdaki genişlemesel fonksiyon eşitliği geçerlidir : ${\ displaystyle \ varphi}$ ${\ displaystyle \ varphi _ {s (p, x)} (y)}$${\ displaystyle f (x, y)}$

${\ displaystyle \ varphi _ {s (p, x)} \ simeq \ lambda y. \ varphi _ {p} (x, y).}$

Daha genel olarak, herhangi m ,  n  > 0 ise, ilkel özyinelemeli işlevi vardır ve m  aşağıdaki gibi davrandığını + 1 argüman: Her Gödel'in sayısı için p kısmi hesaplanabilir fonksiyon ile m  +  n, bağımsız değişkenler ve tüm değerleri X ₁ , …, X _m : ${\ displaystyle S_ {n} ^ {m}}$

${\ displaystyle \ varphi _ {S_ {n} ^ {m} (p, x_ {1}, \ dots, x_ {m})} \ simeq \ lambda y_ {1}, \ dots, y_ {n}. \ varphi _ {p} (x_ {1}, \ dots, x_ {m}, y_ {1}, \ dots, y_ {n}).}$

İşlev s alınabilir, yukarıda tarif olması . ${\ displaystyle S_ {1} ^ {1}}$

Resmi açıklama

Arities Verilen ve her Turing Makinesi için, Arity ait ve girdilerin tüm olası değerleri için , bir Turing makinesi vardır Arity ait böyle, ${\ displaystyle m}$${\ displaystyle n}$${\ displaystyle {\ text {TM}} _ {x}}$${\ displaystyle m + n}$${\ displaystyle y_ {1}, \ noktalar, y_ {m}}$${\ displaystyle {\ text {TM}} _ {k}}$${\ displaystyle n}$

${\ displaystyle \ forall z_ {1}, \ dots, z_ {n}: {\ text {TM}} _ {x} (y_ {1}, \ dots, y_ {m}, z_ {1}, \ noktalar , z_ {n}) = {\ text {TM}} _ {k} (z_ {1}, \ noktalar, z_ {n}).}$

Ayrıca, hesaplama yapılmasına izin veren bir Turing makinesi vardır ve ; gösterilir . ${\ displaystyle S}$${\ displaystyle k}$${\ displaystyle x}$${\ displaystyle y}$${\ displaystyle k = S_ {n} ^ {m} (x, y_ {1}, \ dots, y_ {m})}$

Gayri resmi olarak, değerlerini içine kodlamanın sonucu olan Turing Makinesini bulur . Sonuç, herhangi bir Turing eksiksiz hesaplama modeline genelleştirilir . ${\ displaystyle S}$${\ displaystyle {\ text {TM}} _ {k}}$${\ displaystyle y}$${\ displaystyle {\ text {TM}} _ {x}}$

Misal

Aşağıdaki Lisp kodu , Lisp için s _11'i uygular .

 (defun s11 (f x)
   (let ((y (gensym)))
     (list 'lambda (list y) (list f x y))))

Örneğin, olarak değerlendirilir . (s11 '(lambda (x y) (+ x y)) 3)(lambda (g42) ((lambda (x y) (+ x y)) 3 g42))

Ayrıca bakınız

• Köri
• Kleene'nin özyineleme teoremi
• Kısmi değerlendirme

Referanslar

• Kleene, SC (1936). "Doğal sayıların genel özyinelemeli fonksiyonları" . Mathematische Annalen . 112 (1): 727–742. doi : 10.1007 / BF01565439 .
• Kleene, SC (1938). "Sıra Numaraları İçin Notasyonlarda" (PDF) . Sembolik Mantık Dergisi . 3 : 150–155. (Bu, Odifreddi'nin "Klasik Özyineleme Teorisi" nin 1989 baskısının teorem için 131. sayfada verdiği referanstır .) ${\ displaystyle S_ {n} ^ {m}}$
• Nies, A. (2009). Hesaplanabilirlik ve rastgelelik . Oxford Mantık Kılavuzları. 51 . Oxford: Oxford University Press. ISBN   978-0-19-923076-1 . Zbl   1169.03034 .
• Odifreddi, P. (1999). Klasik Özyineleme Teorisi . Kuzey-Hollanda. ISBN   0-444-87295-7 .
• Rogers, H. (1987) [1967]. Özyinelemeli Fonksiyonlar Teorisi ve Etkili Hesaplanabilirlik . İlk MIT basın ciltsiz baskısı. ISBN   0-262-68052-1 .
• Soare, R. (1987). Özyinelemeli olarak numaralandırılabilen kümeler ve dereceler . Matematiksel Mantıkta Perspektifler. Springer-Verlag. ISBN   3-540-15299-7 .

Dış bağlantılar

• Weisstein, Eric W. "Kleene s - m - n Teoremi" . MathWorld .