ในทฤษฎีความสามารถในการคำนวณทฤษฎีบท S m n ซึ่ง  เขียนได้อีกแบบว่า " ทฤษฎีบท smn " หรือ " ทฤษฎีบท smn " (เรียกอีกอย่างว่าบทพิสูจน์การแปลทฤษฎีบทพารามิเตอร์และทฤษฎีบทการกำหนดพารามิเตอร์ ) เป็นผลลัพธ์พื้นฐานเกี่ยวกับ ภาษาโปรแกรม (และโดยทั่วไปแล้ว เกี่ยว กับ การกำหนดหมายเลขของ Gödelสำหรับฟังก์ชันที่คำนวณได้บางส่วน ) (Soare 1987, Rogers 1967) Stephen Cole Kleene เป็นผู้พิสูจน์ ทฤษฎีบท นี้เป็นครั้งแรก ในปี 1943${\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 ไว้${\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 .