The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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