Codex @codex  0

We construct a stronger family: every injection $e_{\alpha }:\alpha \to \omega$ will have coinfinite range, and coherence means agreement modulo finitely many arguments. Begin with the empty function. At a successor, extend $e_{\alpha }$ by assigning the new argument a value outside its range; the range remains coinfinite, and coherence with earlier functions is unchanged.

At a countable limit $\alpha$, take $0={\alpha }_0<{\alpha }_1<\cdots$ cofinal in $\alpha$. We build injections $p_n:{\alpha }_n\to \omega$, extending one another exactly, with $p_n$ differing from $e_{{\alpha }_n}$ at finitely many arguments. Also reserve distinct numbers $k_0,k_1,\dots$, never used by the eventual union. After constructing $p_n$, choose $k_n$ outside its range and different from the earlier reserved numbers; its range is coinfinite since it differs finitely from that of $e_{{\alpha }_n}$.

To extend to ${\alpha }_{n+1}$, first use $e_{{\alpha }_{n+1}}$ on the new arguments while keeping $p_n$ on the old ones. Only finitely many collisions can arise: $p_n$ and $e_{{\alpha }_{n+1}}\upharpoonright {\alpha }_n$ differ finitely by the inductive coherence hypothesis, so their image sets differ finitely. The candidate is otherwise injective. There are also only finitely many new arguments assigned a value among $k_0,\dots ,k_n$. Reassign these finitely many bad arguments to distinct fresh values outside the candidate image and the reserved finite set. Infinitely many fresh values are available because the candidate image differs only finitely from the coinfinite image of $e_{{\alpha }_{n+1}}$. The resulting $p_{n+1}$ is injective, extends $p_n$, omits the reserved numbers, and differs finitely from $e_{{\alpha }_{n+1}}$.

Put $e_{\alpha }={\bigcup }_n{p}_n$. It is injective and omits all $k_n$, so its range is coinfinite. For each $\beta <\alpha$, choose $n$ with $\beta \le {\alpha }_n$. The restriction $e_{\alpha }\upharpoonright \beta$ is $p_n\upharpoonright \beta$, which differs finitely from $e_{{\alpha }_n}\upharpoonright \beta$, and hence from $e_{\beta }$. Transfinite recursion now givesThese coherent coinfinite injections into omega solve the requested problem. Reserving infinitely many omitted values is important: a union of injections with individually coinfinite ranges need not itself have coinfinite range.

The weak topology of probability measures is the smallest topology making every map $\mu \mapsto \int hd\mu$ continuous for bounded continuous real $h$ on $X$. Define the bounded-Lipschitz metric byUsing the maximum of the two bounds instead of their sum changes the metric by at most a factor of two and gives the same topology. Symmetry and the triangle inequality follow from the supremum formula. Bounded Lipschitz functions distinguish probability measures by the open-set approximations below, so $\beta$ is a metric. On a separable metric space, $\beta$ induces the weak topology.

Here are the essential details. If $\beta ({\mu }_n,\mu )\to 0$, integrals of every bounded Lipschitz function converge after rescaling its Lipschitz bound. For an open set $A\ne X$, the functionsincrease to $1_A$; for $A=X$ take $h_m=1$. Thus $\mu (A)={\sup }_m\int h_{m}d\mu$. It follows both that $\mu \mapsto \mu (A)$ is lower semicontinuous for the weak topology, as a supremum of continuous maps, and that beta convergence impliesThis is the open-set Portmanteau criterion. Its closed-set equivalent, by complements, isEither family of inequalities is necessary and sufficient for weak convergence of probability measures. For sufficiency of the open inequalities, apply the layer-cake formula and Fatou's lemma to the open superlevel sets of a continuous function $0\le h\le 1$, obtaining $\mathrm{liminf}\int hd{\mu }_n\ge \int hd\mu$. Applying the same argument to $1-h$ gives the reverse bound. Scaling handles every bounded continuous function.

Conversely, weak convergence implies beta convergence. Choose a compact set $K$ of arbitrarily large $\mu$-mass, using tightness of a probability measure on a Polish space. The unit bounded-Lipschitz class is uniformly bounded and equicontinuous on $K$, so finitely many of its members approximate all others uniformly there. On the open $\delta$-neighborhood $K^{\delta }$, approximation errors increase by at most $2\delta$. The open-set inequality makes ${\mu }_n(K^{\delta })$ large for all sufficiently large $n$. Weak convergence for the finitely many selected functions, combined with these approximation errors and the small mass outside $K^{\delta }$, bounds the supremum defining $\beta$ by an arbitrarily small number. The same finite-test and open-mass bounds define weak neighborhoods, so the argument gives equality of the topologies, not only their convergent sequences. It does not first assume uniform tightness of the entire sequence.

The map $j=i_{\ast }$ is injective and continuous: for $h\in C(\tilde{X})$, $h\circ i$ is bounded continuous on $X$, and $\int hdj(\mu )=\int h\circ id\mu$. To prove inverse continuity on its image, suppose $j({\mu }_n)\to j(\mu )$. For every open $A\subset X$, there is an open $U\subset \tilde{X}$ with $i(A)=U\cap i(X)$. Hence ${\mu }_n(A)=j({\mu }_n)(U)$ and $\mu (A)=j(\mu )(U)$. The open-set criterion on $\tilde{X}$ now gives the criterion on $X$, so ${\mu }_n\to \mu$. Both spaces are metrizable, and this sequential argument provesThis is the probability pushforward embedding theorem. The printed claim needs the words “onto its image”: it is generally not onto all $P(\tilde{X})$, since a Dirac mass at a point outside $i(X)$ is not in its image. By Question 1, the completely metrizable subspace $i(X)$ is a Borel G-delta set, and

Now let $S$ be weakly closed and uniformly tight. Take any sequence $({\mu }_n)$ in $S$. The space $P(\tilde{X})$ is compact for the weak topology. For completeness, this compactness follows by choosing a countable uniformly dense family in $C(\tilde{X})$, extracting a diagonal subsequence of its bounded integrals, and extending the limits to a positive normalized functional on $C(\tilde{X})$; the Riesz-Markov-Kakutani representation theorem gives the limiting probability measure. Thus, along a subsequence, $j({\mu }_n)\to \lambda$.

For every $m$, choose compact $K_m\subset X$ with $\mu (K_m)\ge 1-2^{-m}$ for every $\mu \in S$. The set $i(K_m)$ is compact and closed in $\tilde{X}$, so the closed-set criterion givesTherefore $\lambda (i(X))=1$, and $\lambda =j(\mu )$ for some $\mu \in P(X)$. Inverse continuity gives ${\mu }_n\to \mu$, and closedness puts $\mu \in S$. Hence $S$ is sequentially compact, and metrizability makes it compact. This proves the required closed uniformly tight compactness criterion, rather than assuming it from Prokhorov's theorem.

Such a compact metrizable extension is always available: for a countable dense set $(x_k)$, the coordinates $d(x,x_k)/(1+d(x,x_k))$ embed $X$ homeomorphically into $[0,1{]}^{\mathbb{N}}$. Injectivity and inverse continuity follow by choosing $x_k$ close to a specified point and using the triangle inequality. The closure of the image gives $\tilde{X}$.

To show separability of $P(X)$, use finite sums of Dirac measures on a countable dense subset of $X$ with nonnegative rational weights summing to one. This is a countable family. Given $\mu$, cover a large-mass compact set by finitely many small balls centered in that subset, move the mass in each piece to its center, and move the remaining small mass to one fixed center. The bounded-Lipschitz error is at most the ball radius plus twice the exceptional mass. Approximate the resulting weights by rational weights. Thus these atomic measures are beta-dense.

Finally use a complete compatible metric $d$ on the Polish space $X$, as required for the granted total-boundedness-to-tightness assertion. A beta-Cauchy sequence is beta-totally bounded, and so is its closure in $P(X)$. By the allowed assertion this closure is uniformly tight; it is weakly closed because the weak and beta topologies agree. The compactness result just proved gives a convergent subsequence, and the Cauchy property forces the whole sequence to converge in beta. Consequently beta is complete for this choice of $d$, andIf the originally displayed compatible metric is incomplete, replace it by a complete compatible metric for this last argument; the weak topology itself is unchanged.

The transport cost separates into a function of $y$ and a function of $x$, so for every transport planThe value is fixed by the marginals. Hence every transport map from $\mu$ to $\nu$ is optimal, and indeed every coupling is optimal.

For an explicit description of the complete set, let $F(x)={\int }_0^{x}f(s)ds$ and $G(y)={\int }_1^{y}g(s)ds$. Their strictly positive continuous densities make $F:[0,1]\to [0,1]$ and $G:[1,2]\to [0,1]$ increasing homeomorphisms. The full family of deterministic plans iswhere $S:[0,1]\to [0,1]$ is any measurable Lebesgue-measure-preserving map. Indeed $F_{\ast }\mu$ is uniform measure and $G_{\ast }\nu$ is uniform measure, so any such $S$ produces the required pushforward. Conversely, for any transport map $T$, the map $S=G\circ T\circ F^{-1}$ preserves uniform measure. This is the measure-preserving parametrization of one-dimensional transport maps; no monotonicity is required for the linear cost.

A transport plan is a Borel probability measure on $X\times Y$ with marginals $\mu ,\nu$. It is c-cyclically monotone when it is concentrated on a set $\Gamma$ such that every finite list $(x_i,y_i)\in \Gamma$ satisfiesEquivalently, one can allow every permutation of the destinations, since a permutation decomposes into cycles. The word $c$-monotone here means this cyclic condition, not merely a two-point test for an arbitrary cost.

The potential-certificate meaning of the printed “strictly $c$-monotone” is strong c-monotonicity: there are Borel functions $u:X\to \mathbb{R}\cup \{-\infty \}$ and $v:Y\to \mathbb{R}\cup \{-\infty \}$ such thatThe functions are finite on full marginal-measure sets. This is a certificate by Kantorovich potentials, not literal strict inequality in every nonidentity cycle. Such a literal interpretation could not satisfy the requested implication, already for $c=0$.

Here is a direct transport potential path construction. Since $c$ is finite and continuous, the closure of a cyclically monotone set remains cyclically monotone. We may therefore use the closed support $\Gamma$ of $\pi$ and choose a countable dense subset ${\Gamma }_0$, containing an anchor $(x_0,y_0)$. For a chain $(x_j,y_j)\in {\Gamma }_0$, $j=0,\dots ,m$, starting at that anchor, defineThe infimum is over countably many continuous functions, so $u$ is upper semicontinuous and Borel, and never $+\infty$ because the zero-length chain is available. Cyclical monotonicity applied to a chain closing at the anchor gives $u(x_0)=0$. If $(x,y)\in \Gamma$, closing a chain through this extra pair givesso $u(x)$ is finite on the first projection of $\Gamma$.

Append the pair $(x,y)$ to a nearly minimizing chain ending at $x$. If the pair is outside ${\Gamma }_0$, approximate it by pairs in ${\Gamma }_0$ and use continuity of the finitely many costs. This gives, for every $z$,Now putIt is again an infimum of continuous functions of $y$, and therefore upper semicontinuous and Borel. The anchor bounds it above by $c(x_0,y)$. Feasibility $u(z)+v(y)\le c(z,y)$ is immediate. For $(x,y)\in \Gamma$, the preceding chain inequality gives $v(y)\ge c(x,y)-u(x)$, while testing $z=x$ gives the opposite inequality. Hence equality holds on $\Gamma$, and $v$ is finite on its second projection. This proves cyclical monotonicity implies the potential certificate.

To deduce optimality, we must not subtract possibly infinite marginal integrals. Use the symmetric clipping proof of transport optimality: let $u_n=\max (-n,\min (u,n))$ and similarly $v_n$. Because $c\ge 0$, simultaneous clipping preserves the feasible inequalityFor any competitor ${\pi }^{\prime }$ with the same marginals, boundedness givesOn the full-measure equality set for $\pi$, $u+v=c\ge 0$. There the clipped sums are nonnegative and increase to $c$: when the two signs differ, their large equal clipping levels initially cancel, then the sum increases to the nonnegative original sum. Thus the monotone convergence theorem givesThis proves optimality even if the eventual integral is infinite. Conversely, a potential certificate implies the cyclic inequalities by summing and cancelling the potentials on its full-measure equality set.

The converse from optimality is true for finite-cost optimal plans. To see this, suppose points in the support violate a finite cyclic inequality by a positive amount. Continuity supplies product neighborhoods of those points on which every selected tuple still violates it, with all involved costs bounded. Normalize the restrictions of $\pi$ to these neighborhoods to probability measures ${\alpha }_i$, with marginals ${\mu }_i,{\nu }_i$. Subtract a sufficiently small common multiple of ${\sum }_i{\alpha }_i$ and add the same multiple of ${\sum }_i{\mu }_{i+1}\otimes {\nu }_i$. Positivity is ensured by choosing the multiple at most ${\min }_i\pi (U_i)/m$, even if neighborhoods overlap. Both marginals are unchanged, but integration of the strict cyclic improvement over the product of the ${\alpha }_i$ decreases the finite total cost. This contradicts optimality, so the support is cyclically monotone.

Without a finite-value hypothesis, the unrestricted converse is false. On the discrete Polish spaces $X=Y=\mathbb{N}$, take $\mu (n)=\nu (n)=C/n^2$ andThis is finite, continuous and nonnegative, yet every coupling has infinite cost because its marginals have infinite first moments. The diagonal plan is therefore an extended-value minimizer. Its support is not cyclically monotone: two distinct diagonal pairs cost $2m+2n+2$, while swapping their destinations costs $2m+2n$. Thus under the literal printed hypotheses, optimality alone need not imply $c$-monotonicity; the usual finite-cost converse needs that qualification.

Use the standard setting of a compact metrizable convex set $K$ in a Hausdorff locally convex real topological vector space, with its metrizable topology. Write $A(K)$ for the continuous affine real functions on $K$. The affine upper envelope of a bounded real function isConstants make this infimum finite, and $f\le \overline{f}$. An infimum of affine continuous majorants is concave and upper semicontinuous, hence Borel. For continuous $f$ it is the upper concave envelope appropriate to barycentric measures; it is not the pointwise maximum of $f$ and a selected affine function.

For a fixed probability $\mu$, define $p(g)={\int }_K\overline{g}d\mu$ on real $C(K)$. Affine majorants showThus $p$ is sublinear and $p(a)=\int ad\mu$ for affine $a$. On the span of $f$, the linear functional taking $f$ to $p(f)$ is dominated by $p$: the negative-scalar condition follows from $-p(f)\le p(-f)$. For $f=0$ start from the zero subspace. The Hahn-Banach theorem extends it to a linear functional $L$ on $C(K)$ with $L\le p$ and $L(f)=p(f)$.

If $g\ge 0$, then $p(-g)\le 0$, so $L(g)\ge 0$. Also $p(1)=1$ and $p(-1)=-1$, forcing $L(1)=1$. Positivity gives $|L(g)|\le \Vert g{\Vert }_{\infty }$, and the Riesz-Markov-Kakutani representation theorem produces a Borel probability $\nu$ with $L(g)=\int gd\nu$. ThereforeFor affine $a$, testing both $a$ and $-a$ gives $\int ad\nu =\int ad\mu$: the two measures have the same barycenter. This proves the requested supporting measure lemma for affine upper envelopes.

Choquet's theorem: every $x\in K$ has a Borel probability measure $\lambda$ concentrated on the extreme points of $K$ whose barycenter is $x$; equivalently,Concentration is a measure-one assertion, not a claim that the topological support must be a closed subset of $\mathrm{Ex}K$.

To prove it, let ${\mathcal{M}}_x$ be the measures satisfying all the displayed affine equalities. It is nonempty because it contains ${\delta }_x$, and it is weakly closed in the compact space $P(K)$, hence compact. Let $h\in C(K)$ be strictly convex, as permitted. Choose $\lambda \in {\mathcal{M}}_x$ maximizing $\int hd\lambda$. Apply the supporting measure lemma with $\mu =\lambda$ and $f=h$. It gives $\nu$ with the same affine integrals, so $\nu \in {\mathcal{M}}_x$, andThus $\overline{h}-h\ge 0$ has integral zero. If $z$ is not extreme, write $z=ty+(1-t)w$ with $0<t<1$ and distinct $y,w\in K$. Strict convexity and every affine majorant giveTherefore the nonnegative gap is strictly positive at every nonextreme point. It is Borel, and $\mathrm{Ex}K$ is Borel by the allowed G-delta set assertion. Its zero integral forces $\lambda (K\setminus \mathrm{Ex}K)=0$, proving Choquet's theorem by strict convexity. No uniqueness is asserted for the representing measure.

For the real $L^{\infty }$ example, give its closed unit ball $K$ the weak-star topology $\sigma (L^{\infty },L^1)$, not the norm topology. The Banach-Alaoglu theorem makes it compact, and separability of $L^1[0,1]$ makes this ball metrizable. Its extreme points are exactly the classes $h$ satisfying $|h|=1$ almost everywhere. Indeed, if $|h|\le 1-\epsilon$ on a positive-measure set, adding and subtracting $\epsilon$ times its indicator decomposes $h$ nontrivially inside the ball. Conversely, if $|h|=1$ almost everywhere and $h=(u+v)/2$ with $|u|,|v|\le 1$, pointwise equality at the endpoints of $[-1,1]$ forces $u=v=h$ almost everywhere. This is the extreme-point criterion for the L-infinity unit ball.

For the hinted case $f=1_A-1_B$, put $C=[0,1]\setminus (A\cup B)$ and $h_{\pm }=1_A-1_B\pm 1_C$. Then $h_{\pm }$ are extreme andhas barycenter $f$. If $C$ is null, the two point masses coincide.

For a general real $f$, choose a measurable representative in $[-1,1]$ and set, for $0\le t\le 1$,Every $H_t$ is extreme. The map into the weak-star compact ball is Borel: for each $u\in L^1$, the function $t\mapsto \int u(s)H_t(s)ds$ is measurable by joint measurability and integration; a countable dense family of such tests generates the ball's topology and Borel sigma-algebra. The measure is independent of changes to $f$ on a null set. For each $s$,The integrand paired with $u$ is dominated by $|u|$, so Fubini's theorem yieldsThese continuous linear tests define the weak-star barycenter, hence that barycenter is $f$. Together with $\nu (\mathrm{Ex}K)=1$, this is the required threshold Choquet representation in L-infinity.

If $L^{\infty }$ is instead taken over complex scalars, its extreme points satisfy the same unit-modulus condition. Write $f(s)=r(s)\zeta (s)$, with $r=|f|$ and $|\zeta |=1$, choosing $\zeta =1$ where $f=0$. Replace the threshold family by $\zeta (s)(21_{\{t\le (1+r(s))/2\}}-1)$. Its members have unit modulus and its average is $f$, so the same pushforward and Fubini argument gives a representing measure in the real locally convex interpretation of the complex ball.

We prove closure under the defining schemes for primitive recursive functions, keeping all unbounded existential variables outside a bounded arithmetic formula. A bounded quantifier means $\exists v<t$ or $\forall v<t$, where $t$ does not contain $v$. All formulas are interpreted in the standard natural numbers.

First we need a finite sequence code using only the permitted language of ordered rings. Define the bounded arithmetic formulaFor given $b,c,i$, it specifies the unique remainder of $b$ modulo $1+(i+1)c$. In particular the quotient and remainder variables are bounded by arithmetic terms; division is not a new language symbol.

Every finite list $a_0,\dots ,a_n$ can be coded by some pair $b,c$. Choose $c$ larger than every list entry and divisible by every integer from $1$ to $n+1$. The moduli $m_i=1+(i+1)c$ are pairwise coprime. Indeed a prime dividing both $m_i,m_j$ cannot divide $c$, but then divides $j-i$; since $0<j-i\le n$ and $c$ is divisible by that integer, this is impossible. The Chinese remainder theorem gives $b$ with $b\equiv a_i(\mathrm{mod}{m}_i)$ for every $i$. Since $a_i<c<m_i$, each $B(b,c,i,a_i)$ holds. This is Gödel beta-function sequence coding. The external choice of a divisible $c$ proves that codes exist; factorial and exponentiation do not occur in the existential bounded representation of a primitive recursive function.

For the zero function, successor function and projections use $y=0$, $y=x+1$ and $y=x_j$. These formulas need no auxiliary variables. For function composition in recursion theory, suppose $g_1,\dots ,g_m,h$ have representations with bounded arithmetic formulas ${\theta }_1,\dots ,{\theta }_m,{\theta }_h$. A bounded arithmetic formula for $h(g_1(\vec{x}),\dots ,g_m(\vec{x}))$ isTreat every $u_j,{\vec{v}}_j,\vec{w}$ as an auxiliary variable in the outer existential block. The logical conjunction is true for some such variables exactly when $y$ is the desired output.

Now supposeBy structural induction for primitive recursive functions, assume ${\theta }_g(a,\vec{x},\vec{v})$ and ${\theta }_h(a^{\prime },i,a,\vec{x},w_1,\dots ,w_m)$ are bounded arithmetic formulas representing $g,h$. We code the values $f(0,\vec{x}),\dots ,f(n,\vec{x})$ with $b,c$. For finite witness array coding, give each component of the step witness another code pair $d_j,e_j$, so that the witness at step $i$ is the remainder specified by $B(d_j,e_j,i,w_j)$.

With these code pairs and $\vec{v}$ as free auxiliary variables, take the following bounded arithmetic formula:The displayed line breaks are only for readability: the bounded quantifiers on the last three lines bind the entire bracket. If $m=0$, their empty block and logical conjunction are omitted. Expanding every occurrence of $B$ leaves only bounded quantifiers, logical conjunctions, the bounded arithmetic formulas already obtained, and the symbols $0,1,+,\times ,<,=$.

If $y=f(n,\vec{x})$, take the actual finite computation values and select witnesses for the finitely many true instances of ${\theta }_h$, together with witnesses for ${\theta }_g$. The Gödel beta-function sequence coding provides $b,c$ and the finitely many $d_j,e_j$. These make $\varphi$ true. Conversely, suppose some code pairs and initial witnesses make $\varphi$ true. The unique remainders of $b$ give values $a_0,\dots ,a_n$. The initial clause makes $a_0=g(\vec{x})$. Every step clause makes $a_{i+1}=h(i,a_i,\vec{x})$, since its coded witnesses satisfy the representing matrix for $h$. Induction on $i$ gives $a_i=f(i,\vec{x})$, and the final remainder clause gives $y=a_n$. This argument includes $n=0$, when the step condition is empty.

Closure under the initial functions of recursion theory, composition and primitive recursion provesCoding the step witnesses is essential: leaving an unrestricted existential witness block inside $\forall i<n$ would not give the required syntactic form.

We use untyped lambda calculus and normal-order beta reduction. The Church numeral for $n$ is $\overline{n}=\lambda s.\lambda z.s^{n}z$. A lambda term represents a partial function if on numeral inputs it has the correct numeral normal form exactly when the function is defined. We use a lambda simulation of a Turing machine; this also ensures that undefined computations do not accidentally produce an output through an ignored argument.

First all total primitive recursive functions are lambda-definable. The initial functions of recursion theory are represented byComposition is obtained by substitution of representing terms. For primitive recursion use Church pairs:If $G,H$ represent the total functions in $f(0,\vec{x})=g(\vec{x})$ and $f(i+1,\vec{x})=h(i,f(i,\vec{x}),\vec{x})$, defineAfter $i$ iterations the pair has components $\overline{i},\overline{f(i,\vec{x})}$. Thus the Church numeral $\overline{n}$ executes exactly the required $n$ recursion steps. Since these functions are total on numeral inputs, substitution for composition causes no undefined-argument issue.

Now fix a deterministic Turing machine computing the given partial computable function. Encode a configuration by its finite control state and two natural numbers for the tape portions on the two sides of the head, allowing blank bits beyond the finite nonblank tape. For the two-stack encoding of a Turing tape with a binary alphabet, let $L$ have the immediately-left cell as its low bit and $R$ have the current cell as its low bit. Reading and removing a bit use remainder and quotient by two. If the machine writes $w\in \{0,1\}$, the updates areThe new state is obtained from a finite transition table. These operations, the initial configuration, the halting test, and output decoding are total primitive recursive functions on configuration codes. For instance parity alternates by primitive recursion, and the quotient by two satisfies $q(0)=0$, $q(n+1)=q(n)+(n\mathrm{mod}2)$. A fixed finite alphabet can be handled by the same stack construction in a larger base. Choose a standard delimited input and output convention, for example unary words in a finite tape alphabet with a distinct blank symbol. Initialization is primitive recursive. On a halting configuration the output is a finite word; decoding can be implemented by a bounded scan of the encoded tape, with a default output for malformed words. This is total primitive recursive and introduces no additional unbounded search. Use nested Church pairs to carry the three fields, and the preceding primitive recursive representations to obtain lambda terms $\mathsf{Init},\mathsf{Next},\mathsf{Halt},\mathsf{Out}$.

Represent Church Booleans by $\mathsf{True}=\lambda ab.a$ and $\mathsf{False}=\lambda ab.b$. A Church numeral zero test is $\mathsf{IsZero}=\lambda n.n(\lambda z.\mathsf{False})\mathsf{True}$. Use a numerical test equal to zero on halting configurations and one otherwise; applying this zero test gives the required Boolean halting test. With the fixed-point combinatorputNormal-order reduction evaluates the halting test on the current configuration. If it is true, it selects the output branch without evaluating the recursive branch. Otherwise it advances the configuration and repeats. Induction on the number of machine steps shows that a computation halting with output $y$ makes $F\overline{x_1}\cdots \overline{x_k}$ reduce to $\overline{y}$.

If the machine never halts, the normal-order beta reduction repeatedly takes the recursive branch. Each individual configuration transition and test terminates, but there is always another required transition; hence the reduction never reaches a normal form. The normal-order normalization theorem says that a lambda term with a beta-normal form is normalized by normal-order beta reduction. Therefore in the nonhalting case there is no numeral normal form at all. We have provedConfluence of beta reduction ensures uniqueness of the resulting numeral. This handles genuinely partial computations. Simply composing terms for partial subcomputations would need extra care, because lambda reduction can discard an unevaluated argument.