Skip to content

Fix: Kernel Substitution Fresh ID Generation

Sankalp Gambhir requested to merge github/fork/sankalpgambhir/kernel-subst-fix into main

Substituting in the presence of bound variables produces dubious results when the fresh ID is not calculated properly.

Consider the following lambda formula

val L = x_1 => \forall x. P(x)

Expected:

L(y) = \forall x. P(x)
L(f(x)) = \forall x. P(x)

Actual:

L(y) = \forall x. P(x)
L(f(x)) = \forall x_1. P(f(x))

During substitution, on reaching the quantifier, the variable x is spotted as occurring in the substitution x_1 => f(x), and based on the discovered set of free variables {x}, is renamed to x_1, leading to the substitution above.

PR adds substitution keys, in this case {x_1} to the free variable pool for renaming, leading to correct results.

Also added a test to account for this.

Merge request reports