Applications of solvability in the λ-calculus


What are applications of solvability / unsolvability, and of operational characterizations of solvability?


Solvability

In the (untyped pure call-by-name) $lambda$-calculus, a closed term is said to be solvable if there is a head context $H=lambda x_1.dots.lambda x_p.square u_1dots u_q$ such that $H(t)to ^* I$ (where $I$ is the identity $lambda x.x$), and unsolvable otherwise.

I am aware of two applications of solvability:

  • When encoding partial recursive functions in the $lambda$-calculus, sending arguments for which the function is not defined to unsolvable terms helps with compositionality (On Undefined and Meaningless in Lambda Definability, Fer-Jan de Vries)

  • When studying observational / contextual equivalence of $lambda$-terms, unsolvable terms are one of the equivalence classes. In some cases, the observational equivalence can be generalized to an observational preorder, and the set of unsolvable terms is then the minimal equivalence class (1). Solvability therefore appears often when building models, e.g. with Böhm trees.

Is solvability useful in other contexts?

(1) This may clash with some definition of solvability in the call-by-value and / or weak / lazy $lambda$-calculus, where people sometimes define “unsolvability of order $n$“. In these settings, “unsolvable” should be understood as meaning “unsolvable of order 0”.


Operational characterization of solvability

A reduction $rightharpoonup$ is said to operationally characterize a set $X$ of $lambda$-terms when the set of weakly normalizing terms with respect to $rightharpoonup$ is exactly $X$, and it is “nice” (for some random definition of “nice” that makes it non-trivial to get an operational characterization of solvability, e.g. deterministic and computable).

In the untyped pure call-by-name $lambda$-calculus, the head reduction operationally characterizes solvability.

I am aware of the following two (potential) applications of the operational characterization:

  • The head reduction is useful to define Böhm trees;

  • If one has two calculi, each with a definition of solvability, proving that a translation preservers solvability is easy: one just needs to extend the translation to (head) contexts, and ensure that the identity is translated to the identity (or something that can be mapped to it by some head context in the target). Proving that it preserves unsolvability, however, is much harder since the target may have more contexts, and so having no context that works in the source does not imply that no context works in the target. If one has an operational characterization of solvability in both calculi, proving the translation preserves unsolvability can be reduced to proving that it respects the reduction that operationally characterizes solvability. This can probably sometimes be extended in some way to prove that observational equivalence is preserved. (I do not have a reference for this application, so a reference for this would be welcome)

Are operational characterizations of solvability useful in other contexts?