Function Property

computation

Definition

Function Property

Fix a type/signature $\tau$ (e.g. ${\mathbb{N}}^k\to \mathbb{N}$ or ${\Sigma }^{\ast }\to {\Sigma }^{\ast }$). Let $F_{\tau }$ be a class of functions of type $\tau$.

A function property is a predicate on functions:

$$P:{\mathcal{F}}_{\tau }\to \{\mathrm{true},\mathrm{false}\}$$

It assigns true/false to entire functions (their input-output behaviour), not to programs.

Extensional vs. Intensional

Extensional

Definition

Extensional Function Property

A function property $P$ is extensional iff it depends only on the computed function (its graph), not on how it’s implemented.

Equivalently: if two Turing machines $M_1,M_2$ compute the same function:

$$F(M_1)=F(M_2)⟹P(F(M_1))=P(F(M_2))$$

Link to original

Intensional

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.

Link to original

Decidability

Decidable

Definition

Decidable Function Property

A function property is decidable iff its code language is decidable.

Link to original

Undecidable

Definition

Undecidable Function Property

A function property is undecidable iff its code language $L_P$ is undecidable.

Link to original