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

[Christian Doczkal]

This is fairly close to the question whether the presentation of CC using (typed) judgmental equality is equivalent to the presentation of CC with (untyped) conversion. This was answered positively for a large class of pure type systems by Siles & Herbelin [1]. Their work encompasses CC, but there is previous work, some of which might also encompass CC. 

Regards,
Christian

[1] Vincent Siles, Hugo Herbelin: Pure Type System conversion is always typable. J. Funct. Program. 22(2): 153-180 (2012) https://doi.org/10.1017/S0956796812000044

On 08/24/2017 02:24 AM, James Koppel wrote:
> [ 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 <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
>>