Talk:Substitution lemma

From The Twelf Project

[edit] Suggestions for points that require clarification

Go wild. --DanielKLee 21:07, 24 September 2006 (MST)

[edit] exchange can be subtle

the current draft suggests that exchange is valid whenever a variable cannot occur in a subsequent type, but unfortunately this simple statement is not true in general. the reason is that the well-formation of a subsequent type may depend on the preceding variable, even if the type itself does not involve that variable! this would come up in situations where the equational theory of types is such as to permit deduction of equations from existence of variables of preceding types, eg x : False, y : Garbage wouldn't permit exchange if the formation of Garbage depended on knowing that x : False is a contradiction!

a related point is strengthening: it is NOT true in general that if a variable doesn't occur, then the variable can be dropped. it is in general a deep property of a type theory that non-occurring variables can be dropped. this was a main complication for the metatheory of lf itself: it is quite non-obvious how to prove strengthening, but this is necessary for some proofs of decidability for beta-eta conversion.

Rwh 21:18, 24 September 2006 (MST)

Point noted. Language modified. --DanielKLee 21:36, 24 September 2006 (MST)