Paper: On the computational power of universally polymorphic recursion (at LICS 1988)

Authors: Assaf J. Kfoury Jerzy Tiuryn Pawel Urzyczyn

Abstract

ML⁺ is an extension of the functional language ML that allows the actual parameters of recursively called functions to have types that are generic instances of the (derived) types of corresponding formal parameters. It is shown that the polymorphism allowed by the original ML can be eliminated without loss of computational power, specifically, it is shown that its computational power (in all interpretations) is the same as that of finitely typed functional programs. It is proved that the polymorphism of ML⁺ cannot be eliminated, in that its computational power far exceeds that of finitely typed functional programs and therefore that of the original ML too

BibTeX

  @InProceedings{KfouryTiurynUrzyczy-Onthecomputationalp,
    author = 	 {Assaf J. Kfoury and Jerzy Tiuryn and Pawel Urzyczyn},
    title = 	 {On the computational power of universally polymorphic recursion},
    booktitle =  {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)},
    year =	 {1988},
    month =	 {July}, 
    pages =      {72--81},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }