We investigate operational characterizations of solvability, i.e. reductions that are normalizing exactly on solvable terms, in calculi with mixed evaluation order (i.e. call-by-name and call-by-value) and pattern-matches. To that end, we generalize a polarized abstract-machine-like calculus. We then operationally characterize solvability in several versions of the calculus (classical, pure intuitionistic, …). In doing so, we illustrate that our calculus is well suited for the study of solvability, that clashes (i.e. pattern-matching failures) are no longer a problem in a polarized calculus, and that operationally characterizing solvability in a classical calculus is easier than in an intuitionistic one. We also show that the main remaining obstacle to the characterization in the full calculus is decidability of separability for “normal-enough” terms.
There is a new version that uses a syntax closer to the λ-calculus.
Timeline: