The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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