The Coq mailing list

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

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