coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Why does CIC have substitution?
- Date: Fri, 25 May 2018 09:12:00 +0000
- Accept-language: en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Thorsten.Altenkirch AT nottingham.ac.uk; spf=Pass smtp.mailfrom=Thorsten.Altenkirch AT nottingham.ac.uk; spf=None smtp.helo=postmaster AT uidappmx01.nottingham.ac.uk
- Ironport-phdr: 9a23:NK96UB8Vtu6AZ/9uRHKM819IXTAuvvDOBiVQ1KB21eocTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZisJyg61VoRKuuxNwzpXOb42JLvdzZL/RcMkYSGdHQ81fVzZBAoS5b4YXEeQBPeFYr5Pmp1sSsxS+AxSnCf/ryj9UmHD226460+U7EQ7a3AwrAtUDvmrUrNXyLqcSSvy1w7fOzTnZc/5W3Sv955bOchAioPGMR65/ccrKxEkpEAPFkkmQqY3jPzOa1uQCqW2b4/B6Wu2zkWIntgJxryGpy8wxhIfJgYcVxUrF9SV/2Is6P8G3SEthbd6jCptQuDmWN41xQsM+X2Fkojw1xaEctZ6mfygHzoksyR3Ha/GfboSE/BHuWPyPLTp3in9pYr2yihio/US91OHxWdG43VVIoyZfkdTBuWoB2wLX58SdVPdx4l+t2TiR2A3Q9u1JJEU5mK7HJ5MgzLM9k5UevEbNHiLzhkn6krWZdksh9+S26+nqYbPrrYKGOYBukAHxKKEul9S/AesmNggOWHCW+fm91LL+50L5WK1Kjvg5k6XFrZzWP8IbpqmlAw9J04Yj7Rm/Dze839Qdh3UINk5KdAiaj4jqI13OIfb4Aumjg1m0jTtn2fPLMqf/DpjCIHXPirjscLhn50JB1gY+wshT55dOBbEAJPLzVFXxtNvdDhIhLQK0w+HnCM9m1oMCR22PBLWVPb/WsV+U+O0vJeqMZI4PuDnhK/go/PjujXglmV8BfKmp25QXaHCiEfRjOUmWe2bjjs0cEWcJpgY+VvDliEWeUT5PYHa/R74z5jYiCI6/EYjDQp2tj6ea0SegHpxWY3hGBUqWHXfpcYWEQfYMZziILs9viDxXHYSmHsUq0gjrvwvnwZJmKPDV82sWr9irgNNy/qjYkQw43T1yFcWUlW+XGTJahGQNEgM227pkvUF7gn6HzaV+gP1CHtwbs89JVR0hKZPaicV+F930WQPbddehTlG6XtSgDjE4S5Q4yJkTYBAuSJ2Zkhnf0n/yUPcunLuRCclsq/OO7z3KP894jk3++uwkhlgiTNFIMDT21Kh46xTSAYHJmkDfnq3saKdOhXeRplfG9nKHuQRjaCA1Sb/MBCBNYEzKsdX/6UPLSvmnAvI6MVkZkJPQGu5xctTsyG5+arLjNdDZOTPjhma8DA6Qw6PUNczsfHkB3SPSCEEB1QkYu2uFZ1Az
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
Hi,
a few years ago we defined PiSigma as a core language for dependent types:
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?
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?
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’
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
— 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.
- [Coq-Club] Why does CIC have substitution?, William J. Bowman, 05/24/2018
- Re: [Coq-Club] Why does CIC have substitution?, Matthieu Sozeau, 05/25/2018
- Re: [Coq-Club] Why does CIC have substitution?, Thorsten Altenkirch, 05/25/2018
- Re: [Coq-Club] Why does CIC have substitution?, William J. Bowman, 05/26/2018
- Re: [Coq-Club] Why does CIC have substitution?, Matthieu Sozeau, 05/26/2018
- Re: [Coq-Club] Why does CIC have substitution?, William J. Bowman, 05/26/2018
- Re: [Coq-Club] Why does CIC have substitution?, Matthieu Sozeau, 05/26/2018
- Re: [Coq-Club] Why does CIC have substitution?, Matthieu Sozeau, 05/25/2018
Archive powered by MHonArc 2.6.18.