[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
The following ignores the category theory part of your question. See: Shankar, A mechanical proof of the Church-Rosser theorem. Journal of the ACM, 35(3):475–522, 1988, where a proof is given of the correspondence between beta on de Bruijn terms and on terms with “raw” (unquotiented) names. You might tie this result into another establishing a connection between the raw and quotiented syntax. Alternatively, my paper with René Vestergaard proves the connection between de Bruijn beta and quotiented beta directly (there is a dash of nominal stuff in there, though). That paper is Norrish & Vestergaard. Proof Pearl: de Bruijn terms really work. Proceedings of TPHOLs 2007, LNCS 4732. (Available from http://nicta.com.au/people/norrishm/attachments/bibliographies_and_papers/2007/tphols2007.pdf) Note that authors from Shankar onwards have not bothered to define arbitrary substitution on dB terms, but have defined a version that assumes they’re substituting into a term underneath a λ-abstraction. This means that when the substitution encounters a small enough variable (which is not the one they’re looking for), its value is decremented to reflect the fact that it is no longer under a λ. This notion of substitution on de Bruijn terms doesn’t correspond to anything nice over “real λ-terms”. I hope these references help, Michael On 05/11/12 07:43, George Cherevichenko wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > Hi > Where can I find a precise description how to interpret typed lambda > calculi with named variables in cartesian closed categories? Or how to > interpret lambda calculi with named variables in lambda calculi with De > Brujn indices? I know how to do that, but I need a link. I need proofs of > the following facts: > 1) Alpha-equal terms correspond to the same term with De Brujn indices (or > the same arrow in CCC). > 2) Substitutions with named variables correspond to substitutions with De > Brujn indices. > I read Altenkirch "Alpha-conversion is easy", should I only refer to this > article? > Please, no nominal logic. > George
