The Coq mailing list

["William J. Bowman" <wjb AT williamjbowman.com>]

I agree that the additional judgment in ΠΣ appears at least as complicated as
substitution.
The definition of "Oleg" in McBride's thesis (chapter 2.1, page 20) is a 
better
comparison to CIC, I think, and *seems to me* somewhat simpler for omitting
substitution.

I guess I was wondering if anyone had considered performance implications (is 
it
more efficient to substitute than to use let as a kind of explicit
substitution?) or philosophical perspectives (is it better to use let as a
object-level representation of substitution than to treat substitution as a
meta-level operation?).

–
William J. Bowman

On Sat, May 26, 2018 at 06:14:36PM +0200, Matthieu Sozeau wrote:
> Right, it's possible to phrase it like this. I understand ΠΣ's motivation
> for turning these x := v into equalities x = v for reflection/conversion
> but I'm not wondering how an intensional type theory like CIC would benefit
> from this. The additional complication in the reduction rules looks
> equivalent to me to the definition of substitution.
> Note that the delta/let reduction rule of CIC is performing immediate
> substitution.
> -- Matthieu
> 
> On Sat, May 26, 2018 at 5:19 PM William J. Bowman 
> <wjb AT williamjbowman.com>
> wrote:
> 
> > Matthieu,
> >
> > Yes that should be one of the closure rules.
> > I suppose this means let is head normal when its body has no more
> > reductions;
> > alternatively, we could have:
> >
> > x := v |- B -> B’
> > -------------------  (when x ∉ FreeVars(B'))
> > let x = v in B -> B’
> >
> > McBride's thesis has a reduction rule like this, and the ΠΣ calculus
> > Thorsten
> > mentioned does something similar via an auxiliary relation that normalizes
> > let
> > bindings.
> >
> > --
> > William J. Bowman
> >
> > On Fri, May 25, 2018 at 10:44:55AM +0200, Matthieu Sozeau wrote:
> > > Hi,
> > >
> > >   What is the reduction rule for let, e.g. for weak head reduction?
> > > If you assume reduction under a local context of definitions, then you
> > get
> > > something like:
> > >
> > > x := v |- B -> B’
> > > -------------------
> > > Let x = v in B -> let x = v in B’
> > >
> > > B' might still contain references to x, so you will need to consider
> > let's
> > > as head normal somehow, no?
> > > — Matthieu
> > >
> > > Le jeu. 24 mai 2018 à 19:31, William J. Bowman 
> > > <wjb AT williamjbowman.com>
> > a
> > > écrit :
> > >
> > > > McBride and McKinna observe that when you have let and δ reduction,
> > > > including substitution is unnecesary.
> > > > (The View From The Left, https://dl.acm.org/citation.cfm?id=967496)
> > > > Instead, we can replace dependent typing rules such as:
> > > >
> > > >   ...
> > > >   ------------------
> > > >   Γ ⊢ e₁ e₂ : B[e₂/x]
> > > >
> > > > By
> > > >
> > > >   ...
> > > >   ------------------
> > > >   Γ ⊢ e₁ e₂ : let x = e₂ in B
> > > >
> > > > And replace substitution in reduction, such as β, by:
> > > >
> > > >   Γ ⊢ (λ x.e) v → let x = v in e
> > > >
> > > > Why does CIC include both let + δ reduction *and* substitution?
> > > >
> > > > --
> > > > William J. Bowman
> > > > Northeastern University
> > > > College of Computer and Information Science
> > > >
> >