×

A filter lambda model and the completeness of type assignment. (English) Zbl 0545.03004

H. B. Curry [in his joint book with R. Feys: Combinatory logic (1958; Zbl 0081.241)], described a formal system assigning types to terms of the type-free \(\lambda\)-calculus. In the ”Open problems” section of Lect. Notes Comput. Sci. 37 (1975; Zbl 0316.00005), D. Scott [Open problem No.114, p. 369] gave a natural semantics for this type assignment and asked whether a completeness result holds. Inspired by M. Coppo, M. Dezani-Ciancaglini, and B. Venneri [Z. Math. Logik Grundlagen Math. 27, 45-58 (1981; Zbl 0479.03006)] the syntax and semantics of types is extended. These types form a partially ordered set with an inf operator. Each term is interpreted as a filter of types. In fact for closed M one has \([[M]]=\{\sigma | \vdash \sigma M\}.\) From this, the completeness for the extended type assignment follows directly. Then it is shown, using a Prawitz normalization argument, that extended type assignment is conservative over that of Curry. It follows that Curry type assignment is also complete with respect to Scott’s semantics. The result has been obtained independently and with a different proof by R. Hindley [Theor. Comput. Sci. 22, 1-17 (1983; Zbl 0512.03009)].

MSC:

03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Automata, languages and programming
[2] The lambda calculus, its syntax and semantics (1981)
[3] Lectures on a mathematical theory of computation (1980)
[4] {\(\lambda\)}-calculus and computer science theory 37 pp 369– (1975)
[5] DOI: 10.1007/3-540-11494-7_15 · doi:10.1007/3-540-11494-7_15
[6] DOI: 10.1002/malq.19810270205 · Zbl 0479.03006 · doi:10.1002/malq.19810270205
[7] To H.B. Curry, Essays in combinatory logic, lambda-calculus and formalism pp 535– (1980)
[8] Theoretical Computer Science · Zbl 0734.68002
[9] DOI: 10.1002/malq.19800261902 · Zbl 0453.03015 · doi:10.1002/malq.19800261902
[10] Combinatory logic. I (1958)
[11] Natural deduction, a proof-theoretical study (1965) · Zbl 0173.00205
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.