ในทฤษฎีความสามารถในการคำนวณ S ม.น.​ ทฤษฎีบท smn หรือเขียนอีกแบบว่า " smn-theorem " หรือ " smn theorem " (เรียกอีกอย่างว่าtranslation lemma , parameter theoremและparameterization theorem ) เป็นผลลัพธ์พื้นฐานเกี่ยวกับภาษาโปรแกรม (และโดยทั่วไปแล้ว เกี่ยว กับ การกำหนดหมายเลขของ Gödelสำหรับฟังก์ชันที่คำนวณได้บางส่วน ) (Soare 1987, Rogers 1967) Stephen Cole Kleeneเป็นผู้พิสูจน์ทฤษฎีบทนี้เป็นครั้งแรกในปี 1943 ชื่อนี้มาจากตัวอักษร n ที่มีตัวห้อยและตัวยกในสูตรดั้งเดิมของทฤษฎีบท (ดูด้านล่าง) ${\displaystyle S_{m}^{n}}$${\displaystyle S}$${\displaystyle n}$${\displaystyle m}$

ในทางปฏิบัติ ทฤษฎีบทนี้กล่าวว่า สำหรับภาษาโปรแกรมที่กำหนดและจำนวนเต็มบวกและจะมีอัลกอริทึม เฉพาะ ที่รับรหัสต้นฉบับของโปรแกรมที่มีตัวแปรอิสระพร้อมกับค่า เป็นอินพุต อัลกอริทึมนี้สร้างรหัสต้นฉบับที่โดยพื้นฐานแล้วจะแทนที่ค่า ลงในตัวแปรอิสระตัวแรก โดยปล่อยให้ตัวแปรที่เหลือเป็นอิสระ ${\displaystyle m}$${\displaystyle n}$${\displaystyle m+n}$${\displaystyle m}$${\displaystyle m}$

รูปแบบพื้นฐานของทฤษฎีบทนี้ใช้ได้กับฟังก์ชันที่มีสองอาร์กิวเมนต์ (Nies 2009, หน้า 6) เมื่อกำหนดหมายเลข Gödel ให้กับฟังก์ชันที่คำนวณได้บางส่วนแล้ว จะมีฟังก์ชันเวียนเกิดดั้งเดิมที่มีสองอาร์กิวเมนต์ซึ่งมีคุณสมบัติดังต่อไปนี้: สำหรับทุกหมายเลข Gödel ของฟังก์ชันที่คำนวณได้บางส่วนที่มีสองอาร์กิวเมนต์ นิพจน์และจะถูกกำหนดสำหรับชุดค่าผสมเดียวกันของจำนวนธรรมชาติและ และค่าของนิพจน์เหล่านี้จะเท่ากันสำหรับทุกชุดค่าผสมดังกล่าว กล่าวอีกนัยหนึ่ง ความเท่าเทียมกันเชิงขยายของฟังก์ชันต่อไปนี้ เป็นจริงสำหรับทุก : ${\displaystyle \varphi }$${\displaystyle s}$${\displaystyle e}$${\displaystyle f}$${\displaystyle \varphi _{s(e,x)}(y)}$${\displaystyle f(x,y)}$${\displaystyle x}$${\displaystyle y}$${\displaystyle x}$

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

โดยทั่วไปแล้ว สำหรับค่าใดๆ ก็ตามจะมีฟังก์ชันเรียกซ้ำแบบดั้งเดิมที่ มี อาร์กิวเมนต์ ซึ่งมีพฤติกรรมดังต่อไปนี้: สำหรับทุกๆ จำนวนเกอเดลของฟังก์ชันที่คำนวณได้บางส่วนที่มีอาร์กิวเมนต์ และค่าทั้งหมดของ: ${\displaystyle m,n>0}$${\displaystyle S_{n}^{m}}$${\displaystyle m+1}$${\displaystyle e}$${\displaystyle m+n}$${\displaystyle x_{1},x_{2},...,x_{m}}$

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

ฟังก์ชันที่อธิบายไว้ข้างต้นสามารถถือได้ว่าเป็น. ${\displaystyle s}$${\displaystyle S_{1}^{1}}$

กำหนดให้จำนวนอาร์กิวเมนต์และสำหรับเครื่องจักรทัวริงทุกเครื่องที่มีจำนวนอาร์กิวเมนต์และสำหรับค่าอินพุตที่เป็นไปได้ทั้งหมดจะมีเครื่องจักรทัวริงที่มีจำนวนอาร์กิวเมนต์ อยู่ เครื่องหนึ่ง เช่นนั้น ${\displaystyle m}$${\displaystyle n}$${\displaystyle {\text{TM}}_{x}}$${\displaystyle m+n}$${\displaystyle y_{1},\dots ,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})={\text{TM}}_{k}(z_{1},\dots ,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}}$

โค้ดLispต่อไปนี้ เป็นการใช้งาน s ₁₁สำหรับ Lisp

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

ตัวอย่างเช่นจะประเมินค่าเป็นโดยที่คือสัญลักษณ์ "ใหม่" (s11'(lambda(xy)(+xy))3)(lambda(g42)((lambda(xy)(+xy))3g42))g42

• เคอร์รี่
• ทฤษฎีการเรียกซ้ำของคลีน
• การประเมินบางส่วน

• ไวส์สไตน์, เอริค ดับเบิลยู. " ทฤษฎีบทs - m - n ของคลีน" . MathWorld .