Substitution does not preserve formula validity

[gebner]

Example

1. Clearly the following formula is valid: P(x) -> ∀x P(x)
2. After substitution it is no longer valid: P(x) -> ∀x P(x)

What is happening here? As you may already have guessed, I'm playing dirty tricks with types here. So let me explain the types of the expressions. The constant P has the sensible type i>o, but x has different types in expression (1).

Concretely the quantifier in (1) ranges over a different type than the argument: P(x:i) -> ∀(x:?a) P(x:i)
Applying the type substitution ?a -> i then gives the non-valid formula (2): P(x:i) -> ∀(x:i) P(x:i)

Here is the code that reproduces this issue:

val f1 = hof"P(#v(x:i)) -> ∀(x:?a) P(#v(x:i))"
val f2 = hof"P(x) -> ∀x P(x)"
assert( f2 == Substitution( Map(), Map( TVar( "a" ) -> ty"i" ) )( f1 ) )

Discussion

Fundamentally, this bug is due to a violation of capture avoidance. In some sense, type substitutions have an infinite domain: they are not the identity on an infinite set of variables. For example, the substitution ?a -> i in the example is not the identity on infinitely many variables:

• x:?a |-> x:i
• x:?a>?a |-> x:i>i
• x:?a>o |-> x:i>o
• etc.

And that's just the variables with the name x!

To come back to capture-avoiding substitution, when applying a substitution to an abstraction λx t, we need to rename x if the substitution maps another variable to x. Without type substitutions, this condition is equivalent to "if x is in the range of the substitution".

However with type substitutions, this condition is not sufficient. In the example, we would need to rename the x:?a in λ(x:?a) P(x:i) even though it does not occur in the range of the substitution. Neither is it sufficient to only rename variables that are modified by the substitution: in the symmetric case of λ(x:i) P(x:?a), we need to rename x:i as well.

(EDIT: I mixed up domain and range.)

Possible solutions

I think there are two potential approaches to fix this issue:

1. We fix substitution so that it produces P(x) -> ∀x_1 P(x) in the example. One way to implement this is to first compute the set of variables that occur in an expression, and add them to the substitution (to artificially make its domain larger). The existing code would then handle the renaming.
2. We change substitution (and free variables) so that they compare variables only by their names. (Substitutions effectively become maps from strings to expressions, and strings to types.) We don't need to compute anything upfront, we can decide whether to rename a variable or not solely based on the range of the substitution and the name of the bound variable. Substitution would then fail on "ill-typed" examples such as the one in Section 1.

IMHO solution 1 is a quick fix, but a bit ugly. For example, substitution no longer commutes with function application (as they may use different renamings).

[gebner]

I've now put in a fix based on solution 1. It was a bit more complicated than expected, you need to add only the free variabkes, otherwise you get an infinite loop due to the bound variable renaming. I also fixed the LK substitution in the same way.

There is still a nondeterministic bug in the code, I'll push a fix when I'm back from lunch.