We investigate the existence of 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. We start by introducing focused call-by-name and call-by-value λ-calculi isomorphic to the intuitionistic fragments of call-by-value and call-by-name λ̅μμ̃, relating them to λ-calculi in which solvability has been operationally characterized, and operationally characterizing solvability in them. We then merge both calculi into a polarized one, explain its relation to the previous calculi, describe how the presence of clashes (i.e. pattern-matching failures) affects solvability, and show how the operational characterization can be adapted the a dynamically typed / bi-typed variant of the calculus that eliminates clashes.
This draft is mostly a translation of an earlier draft from an abstract-machine-like syntax to a λ-calculus-like syntax.
Timeline:
Not all remarks were dealt with yet ↩︎