There is much written about the duality between strict-order (call-by-value) evalutaion for the lambda calculus and the normal-order (call-by-need) evaluation (or semantic equivently, lazy evaluation). In the simply typed lambda calculus, all evaluation eventually terminates, so both evaluation strategies result in the same values. However, when general recursion is added to the simply typed lambda calculus (via a fixpoint operator, for example) then evaluation of some expressions does not terminate. More expressions terminate with normal-order evaluation than with strict-order evaluation. In fact, if evaluation terminates in any order, then it terminates with normal-order evaluation.

I would like to discuss the possibility of a third, even laxer evaluation strategy available for the typed lambda calculus that allows for even more expressions to terminate. I did just say that normal-order evaluation is, in some sense, a best possible evaluation order, so, in order to beat it, we will be adding more redexes that add the commuting conversions.

The typed lambda calculus enjoys certain commuting conversions for case expressions that allow every elimination term to pass through the case expression.
For example, the commuting conversion for the `π₁`

elimination term and the `case`

experssion says that

π₁(case e₀ of σ₁ x. e₁ | σ₂ y. e₂)

converts to

case e₀ of σ₁ x. π₁(e₁) | σ₂ y. π₁(e₂)

These commuting conversions are required so that the subformula property holds.

My understanding is that a corollary of this says that

f(case e₀ of σ₁ x. e₁ | σ₂ y. e₂)

and

case e₀ of σ₁ x. f(e₁) | σ₂ y. f(e₂)

are denotationally equivalent whenever `f`

is a strict function.

I would like to develop a version of the lambda calculus that allows these two expressions to denote the same value for any `f`

.
Call this, the unrestricted commuting conversion property.
A lambda calculus with this property would necessarily be parallel and thus will require a parallel evaluation strategy.
For example, the natural definition of `or`

becomes the parallel-or operation.

or x y := if x then True else y

This definition has the usual short-circuit property that `or True ⊥`

is `True`

where `⊥`

is defined by

⊥ := fix id

If we use the unrestricted commuting conversion property then we also have the that `or ⊥ True`

is `True`

:

or ⊥ True = {definition of or} if ⊥ then True else True = {β-expansion} if ⊥ then const True 〈〉 else const True 〈〉 = {commuting} const True (if ⊥ then 〈〉 else 〈〉) = {β-reduction} True

Hence `or`

is parallel-or.

Other parallel functions, such as the majority function, also follow from their natural definitions.

maj x y z := if x then (or y z) else (and y z)

In this case `maj ⊥ True True`

is `True`

.

maj ⊥ True True = {definition of maj} if ⊥ then (or True True) else (and True True) = {evaluation of (or True True) and (and True True) if ⊥ then True else True = {commuting} True

It is easy to verify that `maj True ⊥ True`

and `maj True True ⊥`

are also both `True`

.

My big question is whether we can devise some nice operational semantics for the lambda calculus that will have the unrestricted commuting conversions property that I desire. Below I document my first attempt at such operational semantics, but, spoiler alert, it does not work.

The usual rule for computing weak head normal form for the case expression `case e₀ of σ₁ x. e₁ | σ₂ y. e₂`

says to first convert `e₀`

to weak head normal form.
If it is `σ₁ e₀′`

then return the weak head normal form of `e₁[x ↦ e₀′]`

.
If it is `σ₂ e₀′`

then return the weak head normal form of `e₂[y ↦ e₀′]`

.
In addition to this rule, I want to add another rule for computing the weak head normal form for the case expression.
This alernative rules says that we compute the weak head normal forms of `e₁`

and `e₂`

.
If we get `C₁ e₁′`

and `C₂ e₂′`

respectively for introduction terms (a.k.a. constructors) `C₁`

and `C₂`

, and
if additionally `C₁`

= `C₂`

then return the following as a weak head normal form, `C₁ (case e₀ of σ₁ x. e₁′ | σ₂ y. e₂′)`

.
If `C₁`

≠ `C₂`

or if we get stuck on a neutral term (e.g. a varaible), then this rule does not apply.

This new rule is in addition to the usual rule for `case`

. Any implementation must run these two rules in parallel because it is possible that either rule (or both) can result in non-termination when recursivly computing weak head normal forms of sub-terms.
I suppose that in case one has unlifted products then when computing the weak head normal form of a `case`

expression having a product type or function type, one can immediately return

〈case e₀ of σ₁ x. π₁ e₁ | σ₂ y. π₁ e₂, case e₀ of σ₁ x. π₂ e₁ | σ₂ y. π₂ e₂〉or

λz. case e₀ of σ₁ x. e₁ z | σ₂ y. e₂ z

This amended computation of weak head normal form seems to work for computing `or`

and `maj`

functions above so that they are non-strict in every argument, but there is another example where even this method of computing weak head normal form is not sufficent.
Consider the functions that implements associativity for the sum type.

assocL : A + (B + C) -> (A + B) + C assocL z := case z of σ₁ a. σ₁ (σ₁ a) | σ₂ bc. (case bc of σ₁ b. σ₁ (σ₂ b) | σ₂ c. σ₂ c) assocR : (A + B) + C -> A + (B + C) assocR z := case z of σ₁ ab. (case ab of σ₁ a. σ₁ a | σ₂ b. σ₂ (σ₁ b)) | σ₂ c. σ₂ (σ₂ c)

Now let us use unrestricted commuting conversions to evaluate `assocR (assocL (σ₂ ⊥))`

.

assocR (assocL (σ₂ ⊥)) = { definition of assocL and case evaluation } assocR (case ⊥. σ₁ b. σ₁ (σ₂ b) | σ₂ c. σ₂ c) = { commuting conversion } case ⊥. σ₁ b. assocR (σ₁ (σ₂ b)) | σ₂ c. assocR (σ₂ c) = { definition of assocR and case evaluations } case ⊥. σ₁ b. σ₂ (σ₁ b) | σ₂ c. σ₂ (σ₂ c) = { commuting conversion } σ₂ (case ⊥. σ₁ b. σ₁ b | σ₂ c. σ₂ c) = { η-contraction for case } σ₂ ⊥

Even if η-contraction is not a reduction rule used for computation, it is still the case that `t`

and `case t. σ₁ b. σ₁ b | σ₂ c. σ₂ c`

should always be dentotationally equivalent.
Anyhow, we see that by using commuting conversions that a weak head normal form of `assocR (assocL (σ₂ ⊥))`

should expose the `σ₂`

constructor.
However, if you apply even my ammended computation of weak head normal form, it will not produce any constructor.

What I find particularly surprising is the domain semantics of `assocL`

and `assocR`

.
`assocL`

seems to map `σ₂ ⊥`

to `⊥`

because no constructor can be exposed.
`assocR`

maps `⊥`

to `⊥`

.
Therefore, according to the denotational semantics, the composition should map `σ₂ ⊥`

to `⊥`

, but as we saw, under parallel evaluation it does not.
It would seem that the naive denotational semantics appears to not capture the semantics of parallel evaluation.
The term `case ⊥. σ₁ b. σ₁ (σ₂ b) | σ₂ c. σ₂ c`

seems to be more defined than ⊥, even though no constructor is available in the head position.

Although my attempt at nice operational semantics failed, I am still confident some nice computation method exists.
At the very least, I believe a rewriting system will work which has all the usual rewriting rules plus a few extra new redexes that says that an elimination term applied to the `case`

expression commutes the elimination term into all of the branches,
and another that says when all branches of a case expression contain the same introduction term, that introduction term is commuted to the outside of the case expression, and maybe also the rules I listed above for unlifted products.
I conjecture this rewriting system is confluent and unrestricted commuting conversions are convertable (probably requiring η-conversions as well).

Without proofs of my conjectures I am a little concerned that this all does not actually work out. There may be some bad interaction with fixpoints that I am not seeing. If this does all work out then shouldn’t I have heard about it by now?