Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I started substitution so that the links to it will no longer be gray, but I leave it more than stubby for the moment. I realize that I need to go and grab something to eat before I can do much more work…
I have added some more chat to substitution explaining how it works in categorical semantics (just trivial stuff)
I wrote a bunch about the syntactic side of substitution.
I don’t think I agree with the terminology here about substitution being an admissible rule. Admissible rule is proof-irrelevant terminology to me, from the premises, there is some derivation of the conclusion, but substitution is fundamentally proof-relevant, it is a construction on proofs/terms.
Instead, I would say that composition is an admissible rule, and that substitution is the operation on terms that witnesses that. If you want to be too cute you could say composition is admissible and substitution is the “admission” :).
I think you can slice it both ways. If you consider the term as being not part of the judgment but rather a syntactic representation of a derivation of that judgment, then yes, substitution on terms is the operation that witnesses the admissibility of a composition/cut rule. But if you view the term as part of the judgment, and the judgment itself as saying “this term has this type”, then the rule itself is substitution (“if this term has this type, and that term has that type, then the substituted term has this other type”).
Coming from programming language theory (but not quite type theory), had a few questions/comments on this page.
That sounds unexpected, as the substitution rule works in type systems without cut elimination/normalization, from STLC + fixpoint to (the PTS with Type : Type or ). I can see that the substitution rule is a special case of cut elimination, but both in simple cases and for arbitrary PTSs*, the substitution rule is proved purely by induction on derivations, and must be proved as part of subject reduction, so much earlier than cut elimination…
*See Lemma 5.2.11 in Barendregt [1992, Lambda Calculi with Types].
Re #7: Some people are happy to refer to forcing out substitutions as “cut elimination” for natural-deduction-style type systems, but I’m also more used to the terminology that cut elimination corresponds to normalization.
The problem is that with the traditional style of typed lambda calculi (including PTSs), an explicit substitution superficially corresponds to a cut, from sequent calculus. But unlike with the sequent calculus, these “cuts” are not the only source of delayed computation.
Probably the term “composition” should’ve been used, in cases where you don’t care about the difference.
I think “∞-equivalence” is just a remnant of a unicode translation issue that we had a little while ago; all such occurrences where -equivalence would make more sense should be fixed to say -equivalence.
Yes, I’ve been guilty (?) of this conflation myself, and may have been the source of the comment on this page. It still seems to me like the logical use of language to refer to admissibility of substitution as a form of cut elimination: after all, the substitution rule is a cut, if the word “cut” can be given any meaning that refers only to the form of a rule itself, and what are you doing but eliminating them? However it seems that, as you say, the phrase “cut elimination” is generally used by type theorists only for a specific sort of elimination of cuts that also does “computation”.
I guess “cut” is just one more thing that has different meanings from a synthetic vs analytic approach. From an analytic perspective starting with sequent calculus, you could say elimination rules have a built-in cut, so full normalization is the closest you can get to cut elimination, since it removes all the interesting cases of cut. (The beta redexes.)
added a Remark (here) showing the substition rule by doing actual substitution (instead of just by the instruction “” to subsitute), which makes it look much more natural, if only one notationally keeps variable dependency around.
(I feel other parts of traditional type theoretic notation could similarly be improved simply by making variable dependency explicit. For example, the traditional notation “” for extended contexts is really a misnomer for “”, which, moreover, is really what the undecorated symbol “” should be taken to denote. Mixing this up often makes discussion of categorical semantics be less transparent than it ought to be.)
1 to 14 of 14