Reducibility of types in typed lambda calculus. Comment on a paper by Richard Statman (Q1104311): Difference between revisions
From MaRDI portal
Created a new Item |
Set OpenAlex properties. |
||
(4 intermediate revisions by 3 users not shown) | |||
Property / reviewed by | |||
Property / reviewed by: Martin W. Bunder / rank | |||
Property / reviewed by | |||
Property / reviewed by: Martin W. Bunder / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/0890-5401(88)90054-5 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2074282135 / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 19:38, 19 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Reducibility of types in typed lambda calculus. Comment on a paper by Richard Statman |
scientific article |
Statements
Reducibility of types in typed lambda calculus. Comment on a paper by Richard Statman (English)
0 references
1988
0 references
If types are built up from the base type 0 using the operation \(\to\), \(\sigma\leq \tau\) is defined by: \((\exists M)M\in \sigma \to \tau \wedge M closed\wedge (\forall N_ 1)(\forall N_ 2)N_ 1,N_ 2\in \sigma \wedge N_ 1, N_ 2\quad closed\to (N_ 1=_{\beta \eta}N_ 2\leftrightarrow MN_ 1=_{\beta \eta}MN_ 2).\sigma <\tau\) iff \(\sigma\leq \tau \wedge \sim \tau \leq \sigma\). \(\sigma\) equivalent to \(\tau\) iff \(\sigma\leq \tau \wedge \tau \leq \sigma.\) \textit{R. Statman} [On the existence of closed terms in typed \(\lambda\)- calculus, I, in: ``To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism'', 511-534 (1980; Zbl 0469.03006)] showed that the equivalence classes of these types are well ordered in type \(\omega +2\) or \(\omega +3.\) The current well written paper shows that type \(\omega +2:\) (((0\(\to 0)\to 0)\to 0)\to 0\to 0\) is strictly less than (0\(\to (0\to 0))\to 0\to 0\) which is the maximal type. Hence these equivalence classes are ordered in type \(\omega +3\).
0 references
lambda calculus
0 references
well order
0 references
types
0 references