Return to Answer

The following is an example from computability theory (more specifically, $\lambda$-calculus) so maybe it's a bit at the border of mathematics proper, but both the question and the answer are so simple and natural that I think it deserves to be mentioned.

We consider the simply-typed $\lambda$-calculus, with types $A,B,\ldots$ generated by a single atom $o$: $$A,B ::= o\mathrel{|} A\to B.$$ Let $A$ be an arbitrary type and let $$ \begin{array}{rcl} \mathsf{Str}[A]&:=& (A\to A)\to(A\to A)\to A\to A, \\ \mathsf{Bool}&:=& o\to o\to o. \end{array} $$ These are the standard types of Church binary strings and booleans, respectively. By well-known results, for all $A$, every closed term $M:\mathsf{Str}[A]\to\mathsf{Bool}$ must decide some language $L\subseteq\{0,1\}^\ast$. Let $\mathsf{ST}\lambda$ be the class of such languages, i.e., $$\mathsf{ST}\lambda:=\{L\subseteq\{0,1\}^\ast\mathrel{|}L\text{ is decidable by some }M:\mathsf{Str}[A]\to\mathsf{Bool}\text{ for some type }A\}.$$ It is natural to ask the following:

Question: Does $\mathsf{ST}\lambda$ correspond to a well-known class?

Surprisingly, very few people know the answer. I myself mentioned in passing this question in front of various audiences of $\lambda$-calculus experts, explicitly saying that a precise characterization of $\mathsf{ST}\lambda$ was missing and that probably this did not correspond to anything remarkable (I even wrote this in a CS Theory StackExchange answer). I never got any reaction. So you can imagine how surprised I was when, a few days ago, after discussing this with two colleagues and realizing that the answer might be the well-known class of regular languages, we found out that we were right and that this had actually been known for more than 20 years:

Theorem. $\mathsf{ST}\lambda=\mathsf{REG}$ (the regular languages on $\{0,1\}$).

This is Theorem 3.4 in the following paper (which is as nice as is unknown):

Gerd G. Hillebrand, Paris C. Kanellakis: On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi. LICS 1996: 253-263.

Very roughly, the proof is based on the fact that the simply-typed $\lambda$-calculus may be interpreted in the category of finite sets (it is cartesian closed) and from this interpretation one may build a finite state automaton for the language decided by a simply-typed $\lambda$-term.

Granted, this is nothing ground-shattering, researchers in the theory of $\lambda$-calculus and programming languages may survive very well (as they do) without knowing it, but I find it doubly suprising that this result is never mentioned: on the one hand, because $\mathsf{ST}\lambda$ ends up being such a simple and universally known class; on the other hand, because this is quite unexpected. Indeed, the class of functions on natural numbers computable by simply-typed $\lambda$-terms is, depending on the convention, either the polynomials with if-then-else (an old result of Schwichtenberg) or a weird subclass of the elementary functions, which includes all towers of exponentials but fails to include, for instance, subtraction (an old result of Statman; if I remember correctly, this class was studied thoroughly by Thierry Joly in his thesis). In both cases, this seems to give the simply-typed $\lambda$-calculus far more power than deciding regular languages.

Edit (22 Nov 2021): I'd like to add that, since I wrote this answer, the above theorem of Hillebrand and Kanellakis has become the starting point of a rich theory exploring the connections between automata and $\lambda$-calculi, showing that the result is more than just a curiosity. An account of this line of research may be found in Lê Thành Dũng "Tito" Nguyễn's Ph.D. thesis.

The following is an example from computability theory (more specifically, $\lambda$-calculus) so maybe it's a bit at the border of mathematics proper, but both the question and the answer are so simple and natural that I think it deserves to be mentioned.

We consider the simply-typed $\lambda$-calculus, with types $A,B,\ldots$ generated by a single atom $o$: $$A,B ::= o\mathrel{|} A\to B.$$ Let $A$ be an arbitrary type and let $$ \begin{array}{rcl} \mathsf{Str}[A]&:=& (A\to A)\to(A\to A)\to A\to A, \\ \mathsf{Bool}&:=& o\to o\to o. \end{array} $$ These are the standard types of Church binary strings and booleans, respectively. By well-known results, for all $A$, every closed term $M:\mathsf{Str}[A]\to\mathsf{Bool}$ must decide some language $L\subseteq\{0,1\}^\ast$. Let $\mathsf{ST}\lambda$ be the class of such languages, i.e., $$\mathsf{ST}\lambda:=\{L\subseteq\{0,1\}^\ast\mathrel{|}L\text{ is decidable by some }M:\mathsf{Str}[A]\to\mathsf{Bool}\text{ for some type }A\}.$$ It is natural to ask the following:

Question: Does $\mathsf{ST}\lambda$ correspond to a well-known class?

Surprisingly, very few people know the answer. I myself mentioned in passing this question in front of various audiences of $\lambda$-calculus experts, explicitly saying that a precise characterization of $\mathsf{ST}\lambda$ was missing and that probably this did not correspond to anything remarkable (I even wrote this in a CS Theory StackExchange answer). I never got any reaction. So you can imagine how surprised I was when, a few days ago, after discussing this with two colleagues and realizing that the answer might be the well-known class of regular languages, we found out that we were right and that this had actually been known for more than 20 years:

Theorem. $\mathsf{ST}\lambda=\mathsf{REG}$ (the regular languages on $\{0,1\}$).

This is Theorem 3.4 in the following paper (which is as nice as is unknown):

Gerd G. Hillebrand, Paris C. Kanellakis: On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi. LICS 1996: 253-263.

Very roughly, the proof is based on the fact that the simply-typed $\lambda$-calculus may be interpreted in the category of finite sets (it is cartesian closed) and from this interpretation one may build a finite state automaton for the language decided by a simply-typed $\lambda$-term.

Granted, this is nothing ground-shattering, researchers in the theory of $\lambda$-calculus and programming languages may survive very well (as they do) without knowing it, but I find it doubly suprising that this result is never mentioned: on the one hand, because $\mathsf{ST}\lambda$ ends up being such a simple and universally known class; on the other hand, because this is quite unexpected. Indeed, the class of functions on natural numbers computable by simply-typed $\lambda$-terms is, depending on the convention, either the polynomials with if-then-else (an old result of Schwichtenberg) or a weird subclass of the elementary functions, which includes all towers of exponentials but fails to include, for instance, subtraction (an old result of Statman; if I remember correctly, this class was studied thoroughly by Thierry Joly in his thesis). In both cases, this seems to give the simply-typed $\lambda$-calculus far more power than deciding regular languages.

Edit (22 Nov 2021): I'd like to add that, since I wrote this answer, the above theorem of Hillebrand and Kanellakis has become the starting point of a rich theory exploring the connections between automata and $\lambda$-calculi, showing that the result is more than just a curiosity. An account of this line of research may be found in Lê Thành Dũng "Tito" Nguyễn's Ph.D. thesis.

The following is an example from computability theory (more specifically, $\lambda$-calculus) so maybe it's a bit at the border of mathematics proper, but both the question and the answer are so simple and natural that I think it deserves to be mentioned.

We consider the simply-typed $\lambda$-calculus, with types $A,B,\ldots$ generated by a single atom $o$: $$A,B ::= o\mathrel{|} A\to B.$$ Let $A$ be an arbitrary type and let $$ \begin{array}{rcl} \mathsf{Str}\{A\}&:=& (A\to A)\to(A\to A)\to A\to A, \\ \mathsf{Bool}&:=& o\to o\to o. \end{array} $$ These are the standard types of Church binary strings and booleans, respectively. By well-known results, for all $A$, every closed term $M:\mathsf{Str}\{A\}\to\mathsf{Bool}$ must decide some language $L\subseteq\{0,1\}^\ast$. Let $\mathsf{ST}\lambda$ be the class of such languages, i.e., $$\mathsf{ST}\lambda:=\{L\subseteq\{0,1\}^\ast\mathrel{|}L\text{ is decidable by some }M:\mathsf{Str}\{A\}\to\mathsf{Bool}\text{ for some type }A\}.$$ It is natural to ask the following:

Question: Does $\mathsf{ST}\lambda$ correspond to a well-known class?

Surprisingly, very few people know the answer. I myself mentioned in passing this question in front of various audiences of $\lambda$-calculus experts, explicitly saying that a precise characterization of $\mathsf{ST}\lambda$ was missing and that probably this did not correspond to anything remarkable (I even wrote this in a CS Theory StackExchange answer). I never got any reaction. So you can imagine how surprised I was when, a few days ago, after discussing this with two colleagues and realizing that the answer might be the well-known class of regular languages, we found out that we were right and that this had actually been known for more than 20 years:

Theorem. $\mathsf{ST}\lambda=\mathsf{REG}$ (the regular languages on $\{0,1\}$).

This is Theorem 3.4 in the following paper (which is as nice as is unknown):

Gerd G. Hillebrand, Paris C. Kanellakis: On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi. LICS 1996: 253-263.

Very roughly, the proof is based on the fact that the simply-typed $\lambda$-calculus may be interpreted in the category of finite sets (it is cartesian closed) and from this interpretation one may build a finite state automaton for the language decided by a simply-typed $\lambda$-term.

Granted, this is nothing ground-shattering, researchers in the theory of $\lambda$-calculus and programming languages may survive very well (as they do) without knowing it, but I find it doubly suprising that this result is never mentioned: on the one hand, because $\mathsf{ST}\lambda$ ends up being such a simple and universally known class; on the other hand, because this is quite unexpected. Indeed, the class of functions on natural numbers computable by simply-typed $\lambda$-terms is, depending on the convention, either the polynomials with if-then-else (an old result of Schwichtenberg) or a weird subclass of the elementary functions, which includes all towers of exponentials but fails to include, for instance, subtraction (an old result of Statman; if I remember correctly, this class was studied thoroughly by Thierry Joly in his thesis). In both cases, this seems to give the simply-typed $\lambda$-calculus far more power than deciding regular languages.

The following is an example from computability theory (more specifically, $\lambda$-calculus) so maybe it's a bit at the border of mathematics proper, but both the question and the answer are so simple and natural that I think it deserves to be mentioned.

We consider the simply-typed $\lambda$-calculus, with types $A,B,\ldots$ generated by a single atom $o$: $$A,B ::= o\mathrel{|} A\to B.$$ Let $A$ be an arbitrary type and let $$ \begin{array}{rcl} \mathsf{Str}[A]&:=& (A\to A)\to(A\to A)\to A\to A, \\ \mathsf{Bool}&:=& o\to o\to o. \end{array} $$ These are the standard types of Church binary strings and booleans, respectively. By well-known results, for all $A$, every closed term $M:\mathsf{Str}[A]\to\mathsf{Bool}$ must decide some language $L\subseteq\{0,1\}^\ast$. Let $\mathsf{ST}\lambda$ be the class of such languages, i.e., $$\mathsf{ST}\lambda:=\{L\subseteq\{0,1\}^\ast\mathrel{|}L\text{ is decidable by some }M:\mathsf{Str}[A]\to\mathsf{Bool}\text{ for some type }A\}.$$ It is natural to ask the following:

Question: Does $\mathsf{ST}\lambda$ correspond to a well-known class?

Surprisingly, very few people know the answer. I myself mentioned in passing this question in front of various audiences of $\lambda$-calculus experts, explicitly saying that a precise characterization of $\mathsf{ST}\lambda$ was missing and that probably this did not correspond to anything remarkable (I even wrote this in a CS Theory StackExchange answer). I never got any reaction. So you can imagine how surprised I was when, a few days ago, after discussing this with two colleagues and realizing that the answer might be the well-known class of regular languages, we found out that we were right and that this had actually been known for more than 20 years:

Theorem. $\mathsf{ST}\lambda=\mathsf{REG}$ (the regular languages on $\{0,1\}$).

This is Theorem 3.4 in the following paper (which is as nice as is unknown):

Gerd G. Hillebrand, Paris C. Kanellakis: On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi. LICS 1996: 253-263.

Very roughly, the proof is based on the fact that the simply-typed $\lambda$-calculus may be interpreted in the category of finite sets (it is cartesian closed) and from this interpretation one may build a finite state automaton for the language decided by a simply-typed $\lambda$-term.

Granted, this is nothing ground-shattering, researchers in the theory of $\lambda$-calculus and programming languages may survive very well (as they do) without knowing it, but I find it doubly suprising that this result is never mentioned: on the one hand, because $\mathsf{ST}\lambda$ ends up being such a simple and universally known class; on the other hand, because this is quite unexpected. Indeed, the class of functions on natural numbers computable by simply-typed $\lambda$-terms is, depending on the convention, either the polynomials with if-then-else (an old result of Schwichtenberg) or a weird subclass of the elementary functions, which includes all towers of exponentials but fails to include, for instance, subtraction (an old result of Statman; if I remember correctly, this class was studied thoroughly by Thierry Joly in his thesis). In both cases, this seems to give the simply-typed $\lambda$-calculus far more power than deciding regular languages.

Edit (22 Nov 2021): I'd like to add that, since I wrote this answer, the above theorem of Hillebrand and Kanellakis has become the starting point of a rich theory exploring the connections between automata and $\lambda$-calculi, showing that the result is more than just a curiosity. An account of this line of research may be found in Lê Thành Dũng "Tito" Nguyễn's Ph.D. thesis.

The following is an example from computability theory (more specifically, $\lambda$-calculus) so maybe it's a bit at the border of mathematics proper, but both the question and the answer are so simple and natural that I think it deserves to be mentioned.

We consider the simply-typed $\lambda$-calculus, with types $A,B,\ldots$ generated by a single atom $o$: $$A,B ::= o\mathrel{|} A\to B.$$ Let $A$ be an arbitrary type and let $$ \begin{array}{rcl} \mathsf{Str}\{A\}&:=& (A\to A)\to(A\to A)\to A\to A, \\ \mathsf{Bool}&:=& o\to o\to o. \end{array} $$ These are the standard types of Church binary strings and booleans, respectively. By well-known results, for all $A$, every closed term $M:\mathsf{Str}\{A\}\to\mathsf{Bool}$ must decide some language $L\subseteq\{0,1\}^\ast$. Let $\mathsf{ST}\lambda$ be the class of such languages, i.e., $$\mathsf{ST}\lambda:=\{L\subseteq\{0,1\}^\ast\mathrel{|}L\text{ is decidable by some }M:\mathsf{Str}\{A\}\to\mathsf{Bool}\text{ for some type }A\}.$$ It is natural to ask the following:

Question: Does $\mathsf{ST}\lambda$ correspond to a well-known class?

Surprisingly, very few people know the answer. I myself mentioned in passing this question in front of various audiences of $\lambda$-calculus experts, explicitly saying that a precise characterization of $\mathsf{ST}\lambda$ was missing and that probably this did not correspond to anything remarkable (I even wrote this in a CS Theory StackExchange answer). I never got any reaction. So you can imagine how surprised I was when, I few days ago, after discussing this with two colleagues and realizing that the answer might be the well-known class of regular languages, we found out that we were right and that this had actually been known for more than 20 years:

Theorem. $\mathsf{ST}\lambda=\mathsf{REG}$ (the regular languages on $\{0,1\}$).

This is Theorem 3.4 in the following paper (which is as nice as is unknown):

Gerd G. Hillebrand, Paris C. Kanellakis: On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi. LICS 1996: 253-263.

Very roughly, the proof is based on the fact that the simply-typed $\lambda$-calculus may be interpreted in the category of finite sets (it is cartesian closed) and from this interpretation one may build a finite state automaton for the language decided by a simply-typed $\lambda$-term.

Granted, this is nothing ground-shattering, researchers in the theory of $\lambda$-calculus and programming languages may survive very well (as they do) without knowing it, but I find it doubly suprising that this result is never mentioned: on the one hand, because $\mathsf{ST}\lambda$ ends up being such a simple and universally known class; on the other hand, because this is quite unexpected. Indeed, the class of functions on natural numbers computable by simply-typed $\lambda$-terms is, depending on the convention, either the polynomials with if-then-else (an old result of Schwichtenberg) or a weird subclass of the elementary functions, which includes all towers of exponentials but fails to include, for instance, subtraction (an old result of Statman; if I remember correctly, this class was studied thoroughly by Thierry Joly in his thesis). In both cases, this seems to give the simply-typed $\lambda$-calculus far more power than deciding regular languages.

The following is an example from computability theory (more specifically, $\lambda$-calculus) so maybe it's a bit at the border of mathematics proper, but both the question and the answer are so simple and natural that I think it deserves to be mentioned.

We consider the simply-typed $\lambda$-calculus, with types $A,B,\ldots$ generated by a single atom $o$: $$A,B ::= o\mathrel{|} A\to B.$$ Let $A$ be an arbitrary type and let $$ \begin{array}{rcl} \mathsf{Str}\{A\}&:=& (A\to A)\to(A\to A)\to A\to A, \\ \mathsf{Bool}&:=& o\to o\to o. \end{array} $$ These are the standard types of Church binary strings and booleans, respectively. By well-known results, for all $A$, every closed term $M:\mathsf{Str}\{A\}\to\mathsf{Bool}$ must decide some language $L\subseteq\{0,1\}^\ast$. Let $\mathsf{ST}\lambda$ be the class of such languages, i.e., $$\mathsf{ST}\lambda:=\{L\subseteq\{0,1\}^\ast\mathrel{|}L\text{ is decidable by some }M:\mathsf{Str}\{A\}\to\mathsf{Bool}\text{ for some type }A\}.$$ It is natural to ask the following:

Question: Does $\mathsf{ST}\lambda$ correspond to a well-known class?

Surprisingly, very few people know the answer. I myself mentioned in passing this question in front of various audiences of $\lambda$-calculus experts, explicitly saying that a precise characterization of $\mathsf{ST}\lambda$ was missing and that probably this did not correspond to anything remarkable (I even wrote this in a CS Theory StackExchange answer). I never got any reaction. So you can imagine how surprised I was when, a few days ago, after discussing this with two colleagues and realizing that the answer might be the well-known class of regular languages, we found out that we were right and that this had actually been known for more than 20 years:

Theorem. $\mathsf{ST}\lambda=\mathsf{REG}$ (the regular languages on $\{0,1\}$).

This is Theorem 3.4 in the following paper (which is as nice as is unknown):

Gerd G. Hillebrand, Paris C. Kanellakis: On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi. LICS 1996: 253-263.

Very roughly, the proof is based on the fact that the simply-typed $\lambda$-calculus may be interpreted in the category of finite sets (it is cartesian closed) and from this interpretation one may build a finite state automaton for the language decided by a simply-typed $\lambda$-term.

Granted, this is nothing ground-shattering, researchers in the theory of $\lambda$-calculus and programming languages may survive very well (as they do) without knowing it, but I find it doubly suprising that this result is never mentioned: on the one hand, because $\mathsf{ST}\lambda$ ends up being such a simple and universally known class; on the other hand, because this is quite unexpected. Indeed, the class of functions on natural numbers computable by simply-typed $\lambda$-terms is, depending on the convention, either the polynomials with if-then-else (an old result of Schwichtenberg) or a weird subclass of the elementary functions, which includes all towers of exponentials but fails to include, for instance, subtraction (an old result of Statman; if I remember correctly, this class was studied thoroughly by Thierry Joly in his thesis). In both cases, this seems to give the simply-typed $\lambda$-calculus far more power than deciding regular languages.