[TYPES] Is one-step conversion rule of CC equivalent to the multi-step one?

[Yang, Yanpeng]

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 <
Thorsten.Altenkirch at nottingham.ac.uk> 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" <
> types-list-bounces at LISTS.SEAS.UPENN.EDU on behalf of yangyp at connect.hku.hk>
> 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.
>
>