On sets of terms with a given intersection type

## Author: Richard Statman

## Paper Information

Title: | On sets of terms with a given intersection type |

Authors: | Richard Statman |

Proceedings: | ITRS Full papers |

Editor: | Michele Pagani |

Keywords: | intersection types, strongly normalizable terms, adequate numeral system |

Abstract: | ABSTRACT. We show (1) For each strongly normalizable lambda term M, with beta eta normal form N, there exists an intersection type A such that in BCD (without top element) we have |-M:A and N is the unique beta-eta normal term s.t.|- N:A. A similar result holds for finite sets of strongly normalizable terms. (2) For each intersection type A, if the set of all closed terms M such that in BCD (without top element) |-M:A is infinite, then when closed under beta-eta conversion this set forms an adequate numeral system for untyped lambda calculus.In particular, all these terms are generated from a single 0 by the application of a successor S, S(...(S0)...) and by beta-eta conversion. |

Pages: | 20 |

Paper: |