[ 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 >
