S-m-n Theorem

Effectively specialize a program index by fixing some inputs, producing a new index whose remaining-input behavior exactly matches the original program with those parameters embedded.

Version

v1 · 2026-08-30 · History

Domain-specific #

2702

Origin domain

computer science

Aliases

Parameter theorem, Parameterization theorem

Core Idea

The S-m-n theorem states that partial evaluation of a computable program can itself be performed effectively at the level of program indices. For an acceptable numbering \(\varphi_e\) of partial computable functions and fixed arities \(m,n\ge1\), there is a total computable function \(s_n^m\) such that

\[ \varphi_{s_n^m(e,a_1,\ldots,a_m)}(x_1,\ldots,x_n) \simeq \varphi_e(a_1,\ldots,a_m,x_1,\ldots,x_n). \]

The symbol \(\simeq\) means both sides are defined with the same value or both diverge. Cutland presents this as Kleene’s S-m-n theorem in the theory of effective program numberings. The theorem is stronger than saying that a specialized program exists: it supplies a uniform total computable transformer from original index and fixed data to specialized index.

Scope of Application

The theorem is foundational in computability theory, effective numberings, recursion-theorem proofs, reductions, and constructions that turn data into code. It formalizes hard-coding: given a program taking configuration and live input, one effectively produces a program with the configuration embedded. Standard computability texts use it alongside universal programs to characterize acceptable programming systems.

It also supplies the theoretical basis for partial evaluation and specialization in programming-language theory, although practical partial evaluators add binding-time analyses and performance goals absent from the theorem. Relativized and injective variants exist, but the canonical identity is the uniform parameter theorem for ordinary partial computable functions.

Clarity

The node separates three levels often blurred: mathematical function, program index, and index transformer. At the function level, fixing arguments is trivial. At the program level, one can informally write a wrapper. At the numbering level, the theorem proves that the wrapper’s code number is computable uniformly from the original code and constants.

Manages Complexity

The theorem turns an informal meta-operation—“write a program with these values built in”—into an internal computable operation on numbers. This lets proofs manipulate programs as data without repeatedly returning to machine syntax. Arity bookkeeping is captured by the superscript/subscript convention, and extensional equivalence shields the proof from irrelevant code layout.

Abstract Reasoning

Given a computable relation represented by an indexed program, S-m-n lets a proof freeze construction parameters and obtain a uniformly indexed family. This supports many-one reductions where instances are compiled into programs, computable enumerations of parameterized behaviors, and diagonal constructions that need code depending on its own or another index.

Knowledge Transfer

The exact theorem transfers across acceptable Turing-machine, register-machine, lambda-calculus, and general-purpose programming-system numberings because effective compilation relates them. Source syntax changes while source index, static parameters, residual inputs, total transformer, and extensional equality remain.

Beyond computability, “bind some inputs now, others later” recurs in closures and templates, but those are structural relatives. S-m-n remains domain-specific because Gödel numbering, partial computability, and uniform index production are indispensable.

Relationships to Other Abstractions

Current abstraction S-m-n Theorem Domain-specific

Parents (1) — more general patterns this builds on

• S-m-n Theorem presupposes Computability Prime

  S-m-n composes Computability because it establishes an effective operation on program indices.

Hierarchy paths (2) — routes to 2 parentless roots

• S-m-n Theorem → Computability → Algorithm → Function (Mapping)

Show alternative path (1)

Neighborhood in Abstraction Space

S-m-n Theorem sits in a sparse region of the domain-specific corpus (87^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Computational Number Theory & Enumeration (13 abstractions)

Nearest neighbors

• Automatic Differentiation — 0.80
• Pseudorandom Number Generator — 0.80
• Divisor Function — 0.80
• Bessel Function — 0.79
• Condensed Detachment — 0.79

Computed from structural-signature embeddings · 2026-09-08