Closed bitonic closed 9 years ago
x
doesn't appear in α β
so it's not clear what you're aiming at here.
Right... I thought there were cases where the expansion was a problem but actually I think it was a consequence of how I performed the pruning in my code.
Given
Let's say that we want to prune variable
x
inα β
. Everything should go smoothly, however if we curryβ
, which we must do in the general case for unification to be complete, we're left withUsually we never attempt to prune λ-arguments to a meta-variable, but here we really should. We can't eta-contract the abstraction over
γ
.We need a better way to prune under abstractions, but I'm not sure how to proceed.