Hah! I think I have completeness of this algorithm actually proved now.

Two major lessons learned: One, if you have a substitution lemma, make for god-damned sure that every last case of it works early, before you need to change a metric fuckton of notation when you realize they don't. Two, if you have some machinery that satisfies some nice property and you are feeling all smug that you've proved something, make for god-damend sure that it is the property you actually need for the rest of the machinery to work before you need to change a second metric fuckton of notation when you realize it isn't.

Earlier this evening watched "Wet Hot American Summer" with people around the house. Pretty funny, recommend it highly if you are in the mood for a cheesy 80's-movie parody. Parenthesize those last three words any way you like.

Question for the types crowd: Let Δ be the type of functions f : nat -> nat such that f(x) <= x. This can be thought of as the infinite product type 1 x 2 x 3 x 4 x ... or a dependent product or whatever you prefer.

Now the idea of having a type operator which is somehow "a thing that takes τ to Δ x exp(τ)" where exp is to be read as, yes, the exponential function, is not such a crazy thing if we think of power series. Say Δ(i) is the "ith truncation" of Δ (i + 1) x (i + 2) x ... So we could say

Δ x exp(τ) = Σ_{i} Δ(i) x τ^{i}

(to reflect the power series exp(x) = 1 + x + x^2/2! + x^3/3! + ...)

Now we also have a nice power series for -ln(1-x),

1 + x + x^2/2 + x^3 / 3

And moreover -ln(1-x) = ln(1/(1-x)), and α list is a reasonable interpretation of 1/(1-α) since it is the type solution of β = 1 + α x β just as 1/(1-x) is the solution of y = 1 + xy.

In this way we can come up with a reasonable interpretation in types of Δ x ln(τ list), as

Σ_{i} Δ'(i) x τ^{i}

where Δ'(i) is the infinite product 1 x 2 x 3 x 4 x ... with the ith term absent.

Given all this nonsense, one might therefore hope, by way of hand-waving and "algebra", that the type Δ x (Δ x σ -> τ list) (where the arrow is the function type constructor, think of it as an exponentiation) might somehow be related to the type Δ x exp(Δ x ln(τ list) x σ)

Ideally by an isomorphism, but I doubt things work out that cleanly. Any ideas how to do this? I have this vague feeling that someone already did this sort of thing in the literature.