Intensional Function Property

computation

Definition

Intensional Function Property

Fix a representation of computable functions (e.g. Turing machines). A function property is intensional if it is a predicate on machine encodings

$$R:\{⟨M⟩\}\to \{\mathrm{true},\mathrm{false}\}$$

that is not invariant under extensional equality of the computed function.

Equivalently, there exists $M_1,M_2$ with the same computed function $F(M_1)=F(M_2)$ but $R(⟨M_1⟩)\ne R(⟨M_2⟩)$.

$R$ depends on how the function is implemented, not only on the input-output mapping.

Examples

Intensional Function Property

• The machine halts in $\le 100$ steps on every input.
• The program has $\le 5$ states / contains instruction $X$.
• On empty input, the machine writes on $>100$ cells.
• The implementation is written as primitive-recursive expression