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

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Beta equivalence is the reflexive symmetric transitive closure of one-step
beta reduction. Every pair of beta-equivalent terms is witnessed by a chain
of zero or more one-step beta reductions or inverse one-step beta
reductions. That immediately implies that every use of the Conv rule could
be replaced by zero or more uses of the Conv-Step rule.

That is, unless it's somehow possible for one of the intermediate terms to
be ill-typed (i.e.: fail the A : s condition). Presumably not doing so is a
prerequisite to having beta-reduction be well-defined.

On Wed, Aug 23, 2017 at 4:21 AM, Yang, Yanpeng <[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
>