| ||||
| ||||
![]() Title:On sets of terms with a given intersection type Authors:Richard Statman Conference:ITRS 2018 Tags:adequate numeral system, intersection types and strongly normalizable terms 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. On sets of terms with a given intersection type ![]() On sets of terms with a given intersection type | ||||
Copyright © 2002 – 2025 EasyChair |