The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Hi,

a few years ago we defined PiSigma as a core language for dependent types:

http://www.cs.nott.ac.uk/~psztxa/publ/pisigma-new.pdf

It only uses let (actually letrec) instead of substitutions. 

In particular the beta rule uses let

D |- t ~> \x->t'  x#D D |- (let x=u in t') ~> v

-----------------------------------------------------------------

D |- (\x -> t) u ~> v

here D is a context of definitions, x#D means x is fresh wrt D.

Thorsten

From: <coq-club-request AT inria.fr> on behalf of Matthieu Sozeau <mattam AT mattam.org>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Friday, 25 May 2018 at 09:44
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Why does CIC have substitution?

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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.