[TYPES] Please give me a link. Is alpha-conversion easy or not?

[Michael Norrish]

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