Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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

    diff, v11, current

    • CommentRowNumber7.
    • CommentAuthorpggiarrusso
    • CommentTimeAug 4th 2019

    Coming from programming language theory (but not quite type theory), had a few questions/comments on this page.

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

  2. Added redirects for substitution rule and substitution rules

    Anonymous

    diff, v16, current

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMar 26th 2023
    • (edited Mar 26th 2023)

    added a Remark (here) showing the substition rule by doing actual substitution (instead of just by the instruction “[t/x][t/x]” 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 “Γ.A\Gamma.A” for extended contexts is really a misnomer for “(γ:Γ)×A γ(\gamma \colon \Gamma) \times A_\gamma”, which, moreover, is really what the undecorated symbol “AA” should be taken to denote. Mixing this up often makes discussion of categorical semantics be less transparent than it ought to be.)

    diff, v17, current

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeMar 26th 2023

    added references for the type-theoretic inference rule

    (now the first three here)

    diff, v17, current