[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear James and Thorsten, Thanks a lot for your replies! I feel sorry that there is a typo in rules that I presented in my first email, as pointed by Thorsten's reply. The second premise should be "G |- B : s" instead of "G |- A : s", as the latter one is usually admissible by the lemma "Correctness of Types". The following discussion is based on the corrected rules: G |- e : A G |- B : s # Should be B here A ==beta B ------------------- Conv G |- e : B G |- e : A G |- B : s # Should be B here A --> B \/ B --> A -------------------------- Conv-Step G |- e : B > If you want to use beta-equality as suggested you need to make sure that both types are well-typed, that is you have to add the assumption G |- B : s in both rules. My apologies. I should use the corrected rules above. Let's discuss if these two rules are equivalent. > That is, unless it's somehow possible for one of the intermediate terms to be ill-typed (i.e.: fail the A : s condition). I have the same concern here. In the original "Conv" rule, the premises only ensure B is well-typed but not the intermediate types which need to be well-typed in "Conv-Step" rules. Considering a reduction sequence A --> C --> B, we can apply "Conv" rule once and check if A and B are well-typed, but need to apply "Conv-Step" twice and check all A, B and C. Unless we know subject reduction holds in the system with "Conv-Step", we just need to check A and B. But I got stuck when tried to prove subject reduction since I cannot work out inversion lemmas using the "Conv-Step" rule. Any ideas on fixing the proof? Thanks again! Regards, Yanpeng On Thu, Aug 24, 2017 at 5:52 PM, Thorsten Altenkirch < [email protected]> wrote: > Conversion should be defined as a judgement only including typed terms > otherwise it is not clear what the system means semantically. > > If you want to use beta-equality as suggested you need to make sure that > both types are well-typed, that is you have to add the assumption G |- B : > s in both rules. Otherwise you get untypable types which make no sense and > do not correspond to typing judgement in the reference system using > judgements. > > Thorsten > > On 23/08/2017, 09:21, "Types-list on behalf of Yang, Yanpeng" < > [email protected] on behalf of [email protected]> > wrote: > > [ The Types Forum, http://lists.seas.upenn.edu/ > mailman/listinfo/types-list ] > > Dear all, > > The conversion rule of the Calculus of Constructions (CC) is usually > defined as follows: > > G |- e : A > G |- A : s > A ==beta B > ------------------- Conv > G |- e : B > > I wonder if this rule is equivalent to the one using *one-step* beta > reduction: > > G |- e : A > G |- A : s > A --> B \/ B --> A > -------------------------- Conv-Step > G |- e : B > > This "Conv-Step" rule is shown in Geuvers' paper [1, Definition 4.1] > but > which never mentions if it is equivalent to the original "Conv" rule. > > So, my question is: has it ever been proved that the two conversion > rules > are equivalent? If so, what is the appropriate article to refer to for > this > proof? > > Thanks a lot! > > Sincerely, > Yanpeng > > [1] Geuvers, Herman. "A short and flexible proof of Strong > Normalization > for the Calculus of Constructions." International Workshop on Types for > Proofs and Programs. Springer, Berlin, Heidelberg, 1994. > URL: http://flint.cs.yale.edu/trifonov/cs629/Geuvers-SN-CC-2up.ps > > > > > > > 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 send it back to me, and immediately delete it. > > Please do not use, copy or disclose the information contained in this > message or in any attachment. Any views or opinions expressed by the > author of this email do not necessarily reflect the views of the > University of Nottingham. > > This message has been checked for viruses but the contents of an > attachment may still contain software viruses which could damage your > computer system, you are advised to perform your own checks. Email > communications with the University of Nottingham may be monitored as > permitted by UK legislation. > >
