WikiDer > Смн теоремасы - Википедия

Жылы есептеу теориясы The S м
n  теорема, (деп те аталады аударма леммасы, параметр теоремасы, және параметризация теоремасы) туралы негізгі нәтиже болып табылады бағдарламалау тілдері (және, жалпы, Gödel нөмірлері туралы есептелетін функциялар) (Soare 1987, Rogers 1967). Мұны алдымен дәлелдеді Стивен Коул Клейн (1943). Аты S м
n  пайда болуынан пайда болады S индекспен n және жоғарғы әріп м теореманың түпнұсқалық тұжырымдамасында (төменде қараңыз).

Практикалық тұрғыдан теорема берілген бағдарламалау тілі мен натурал сандар үшін дейді м және n, белгілі бір нәрсе бар алгоритм кіріс ретінде қабылдайды бастапқы код бағдарламасының м + n еркін айнымалылар, бірге м құндылықтар. Бұл алгоритм мәндердің біріншісін тиімді алмастыратын бастапқы код жасайды м қалған айнымалыларды бос қалдырып, еркін айнымалылар.

Егжей

Теореманың негізгі формасы екі аргументтің функцияларына қолданылады (Nies 2009, 6-бет). Годель нөмірі берілген ${ displaystyle varphi}$ рекурсивті функциялар, а бар қарабайыр рекурсивті функция с келесі сипаттағы екі аргумент: әр Gödel нөмірі үшін б ішінара есептелетін функцияның f екі дәлелмен, өрнектермен ${ displaystyle varphi _ {s (p, x)} (y)}$ және ${ displaystyle f (x, y)}$ натурал сандардың бірдей комбинациясы үшін анықталады х және ж, және олардың мәні кез келген осындай комбинацияға тең. Басқаша айтқанда, келесі кеңейтілген теңдік функциялар әрқайсысына сәйкес келеді х:

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

Жалпы, кез келген үшін м, n > 0, қарабайыр рекурсивті функция бар ${ displaystyle S_ {n} ^ {m}}$ туралы м + 1 аргумент келесідей әрекет етеді: әр Gödel нөмірі үшін б ішінара есептелетін функцияның м + n аргументтер және барлық мәндері х₁, …, х_м:

${ displaystyle varphi _ {S_ {n} ^ {m} (p, x_ {1}, dots, x_ {m})} simeq lambda y_ {1}, dots, y_ {n}. varphi _ {p} (x_ {1}, нүктелер, x_ {m}, y_ {1}, нүктелер, y_ {n}).}$

Функция с жоғарыда сипатталған деп қабылдауға болады ${ displaystyle S_ {1} ^ {1}}$.

Ресми мәлімдеме

Берілген келісімдер ${ displaystyle m}$ және ${ displaystyle n}$, әр Тьюринг машинасы үшін ${ displaystyle { text {TM}} _ {x}}$ ақыл-ой ${ displaystyle m + n}$ және кірістердің барлық мүмкін мәндері үшін ${ displaystyle y_ {1}, нүктелер, 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}, dots , z_ {n}) = { мәтін {TM}} _ {k} (z_ {1}, нүктелер, z_ {n}).}$

Сонымен қатар, Тьюринг машинасы бар ${ displaystyle S}$ бұл мүмкіндік береді ${ displaystyle k}$ бастап есептелуі керек ${ displaystyle x}$ және ${ displaystyle y}$; ол белгіленеді ${ displaystyle k = S_ {n} ^ {m} (x, y_ {1}, dots, y_ {m})}$.

Ресми емес, ${ displaystyle S}$ Тьюринг машинасын табады ${ displaystyle { text {TM}} _ {k}}$ бұл мәндерін қатаң кодтаудың нәтижесі ${ displaystyle y}$ ішіне ${ displaystyle { text {TM}} _ {x}}$. Нәтиже кез-келгенге жалпыланады Тюринг-аяқталған есептеу моделі.

Мысал

Келесісі Лисп кодты жүзеге асырады₁₁ Лисп үшін.

 (бас тарту s11 (f х)   (рұқсат етіңіз ((ж (генсим)))     (тізім 'лямбда (тізім ж) (тізім f х ж))))

Мысалға, (s11 '(лямбда (х ж) (+ х ж)) 3) бағалайды (лямбда (g42) ((лямбда (х ж) (+ х ж)) 3 g42)).

Сондай-ақ қараңыз

• Карри
• Клейннің рекурсиялық теоремасы
• Ішінара бағалау

Әдебиеттер тізімі

• Kleene, S. C. (1936). «Натурал сандардың жалпы рекурсивтік функциялары». Mathematische Annalen. 112 (1): 727–742. дои:10.1007 / BF01565439.
• Kleene, S. C. (1938). «Реттік сандарға арналған белгілер туралы» (PDF). The Символикалық логика журналы. 3: 150–155. (Бұл Одифреддинің «Классикалық рекурсия теориясының» 1989 жылғы басылымында 131 б. Келтірілген сілтеме. ${ displaystyle S_ {n} ^ {m}}$ теорема.)
• Nies, A. (2009). Есептеу және кездейсоқтық. Оксфордтың логикалық нұсқаулықтары. 51. Оксфорд: Оксфорд университетінің баспасы. ISBN 978-0-19-923076-1. Zbl 1169.03034.
• Одифредди, П. (1999). Классикалық рекурсия теориясы. Солтүстік-Голландия. ISBN 0-444-87295-7.
• Роджерс, Х. (1987) [1967]. Рекурсивті функциялар теориясы және тиімді есептеу. MIT-тің алғашқы қағаздан шыққан басылымы. ISBN 0-262-68052-1.
• Soare, R. (1987). Рекурсивті түрде есептелетін жиынтықтар мен дәрежелер. Математикалық логиканың перспективалары. Шпрингер-Верлаг. ISBN 3-540-15299-7.

Сыртқы сілтемелер

• Вайсштейн, Эрик В. «Клиннің с-м-n Теорема ». MathWorld.