patternMinor
Is there any meaning behind the classification of "λ-terms" in classes such as "church number" and "church list"?
Viewed 0 times
meaningsuchthenumberanyclassificationtermsclassesbehindand
Problem
λ-calculus terms can be informally/intuitively categorized, such as:
That is, while the untyped lambda calculus obviously doesn't have explicit types, one can certainly recognize patterns on terms and categorize them based on their behavior - as if those had a type. When you say: "a church number is a function that applies another function
(λ f x . (f (f (f x))))) is a church natural (3)(λ a b . a) is a church boolean (true)(λ c n . (c 1 (c 2 (c 3 n)))) is a church list ([1,2,3])(λ s z . (s (λ s z . (s (λ s z . (s (λ s z . z))))))) is a peano natural (3)That is, while the untyped lambda calculus obviously doesn't have explicit types, one can certainly recognize patterns on terms and categorize them based on their behavior - as if those had a type. When you say: "a church number is a function that applies another function
n times to an argument" you are informally characterizing a wide range of λ-terms. My question is: is there any way to formalize that intuition? Any system/theory that meaningfully categorizes (untyped) λ-terms?Solution
Several observations can be made based on your remarks:
-
In System F, every data type can be given an encoding using polymorphic types, e.g. $\mathrm{Bool}$ can be defined as the type
$$\forall A.A\rightarrow A\rightarrow A$$
On the other hand, certain terms (not all of course) can be given a principal type in system F, e.g.
$$\lambda ab.a $$
can be given the type $\forall AB.A\rightarrow B \rightarrow A$. But you can now notice that this is a generalization of the type $\forall A.A \rightarrow A \rightarrow A$, and this happens to be the most general type it shares with $\lambda a b.b$, which is of course the polymorphic encoding of $\mathrm{Bool}$. In this way, one can always attempt to assign the most general type to a term, and then check to see if this happens to be (a generalization of) the polymorphic encoding of a datatype.
-
Intersection type systems are usually undecidable type systems assigning types to pure $\lambda$-terms that have the remarkable property of classifying their behavior: in particular the most simple such system is complete for strong normalization: a term has a type iff it is SN.
In intersection type systems, it is always possible to interpret the set of all types of a term (ordered by the sub-typing relation) as a representation of the behavior of that term. In particular, there is a close correspondence between the various domain theory models of the pure $\lambda$-calculus and various intersection typing systems. See for example Intersection Types and Lambda Theories for an overview.
-
In System F, every data type can be given an encoding using polymorphic types, e.g. $\mathrm{Bool}$ can be defined as the type
$$\forall A.A\rightarrow A\rightarrow A$$
On the other hand, certain terms (not all of course) can be given a principal type in system F, e.g.
$$\lambda ab.a $$
can be given the type $\forall AB.A\rightarrow B \rightarrow A$. But you can now notice that this is a generalization of the type $\forall A.A \rightarrow A \rightarrow A$, and this happens to be the most general type it shares with $\lambda a b.b$, which is of course the polymorphic encoding of $\mathrm{Bool}$. In this way, one can always attempt to assign the most general type to a term, and then check to see if this happens to be (a generalization of) the polymorphic encoding of a datatype.
-
Intersection type systems are usually undecidable type systems assigning types to pure $\lambda$-terms that have the remarkable property of classifying their behavior: in particular the most simple such system is complete for strong normalization: a term has a type iff it is SN.
In intersection type systems, it is always possible to interpret the set of all types of a term (ordered by the sub-typing relation) as a representation of the behavior of that term. In particular, there is a close correspondence between the various domain theory models of the pure $\lambda$-calculus and various intersection typing systems. See for example Intersection Types and Lambda Theories for an overview.
Context
StackExchange Computer Science Q#44819, answer score: 5
Revisions (0)
No revisions yet.