Logic in Computer Science (LICS 1993)

Paper: Adequacy for untyped translations of typed λ-calculi (at LICS 1993)

Authors: Wesley Phoa

Abstract

PCF is a simply typed λ-calculus with ground types ι (natural numbers) and ο (Booleans); there are no type variables and ⇒ is the only type constructor. There is a natural way to translate any PCF term t into an untyped λ-expression Λ(t), such that if t is a program, i.e. a closed term of ground type (say integer type) and t ⇒_N n̅ then Λ(t) ⇒_β c_n, where ⇒_N denotes call-by-name evaluation and c_n denotes the nth Church numeral. This paper contains a proof of the converse: if Λ(t) ⇒_β c_n then t ⇒_N n̅; this tells us that the translation is adequate. The proof is semantic, and uses synthetic domain theory to reduce the question to the original Plotkin/Sazonov adequacy theorem for standard domain models of call-by-name PCF. This argument generalises easily to extensions of PCF which can be translated into the untyped λ-calculus: we illustrate this by proving an analogous result for a `second-order' PCF with type quantification. We also discuss how to extend the result to versions of PCF with recursive types and subtyping

BibTeX

  @InProceedings{Phoa-Adequacyforuntypedt,
    author = 	 {Wesley Phoa},
    title = 	 {Adequacy for untyped translations of typed λ-calculi},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {287--295},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }