# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeMay 9th 2012
• (edited May 9th 2012)

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…

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeMay 11th 2012

I have added some more chat to substitution explaining how it works in categorical semantics (just trivial stuff)

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeJun 21st 2012

I wrote a bunch about the syntactic side of substitution.

• CommentRowNumber4.
• CommentAuthormaxsnew
• CommentTimeAug 3rd 2017

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” :).

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeAug 3rd 2017

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”).

1. Minor (Replace ∞-equivalent with alpha-equivalent, which is the right notion)

Paolo G. Giarrusso

• CommentRowNumber7.
• CommentAuthorpggiarrusso
• CommentTimeAug 4th 2019

• Does ∞-equivalence exist? I’m sure alpha-equivalence is correct in its place, but ∞-equivalence is still mentioned in some redirects.
• > The substition rule is closely related to the cut rule, and admissibility of such rules is generally proven by cut elimination.

That sounds unexpected, as the substitution rule works in type systems without cut elimination/normalization, from STLC + fixpoint to $\lambda^*$ (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].

• CommentRowNumber8.
• CommentAuthoratmacen
• CommentTimeAug 4th 2019

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.

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeAug 5th 2019

I think “∞-equivalence” is just a remnant of a unicode translation issue that we had a little while ago; all such occurrences where $\alpha$-equivalence would make more sense should be fixed to say $\alpha$-equivalence.

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeAug 8th 2019

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”.

• CommentRowNumber11.
• CommentAuthoratmacen
• CommentTimeAug 8th 2019

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.)