Mathematics and Computation

A blog about mathematics for computers

Interesting higher-order functionals

Spaces of higher-order functions are fascinating mathematical objects that we do not know enough about. What are they and what is known about them?

What are functionals

Functionals are higer-order functions, i.e., functions that take functions as arguments or return them as results. Common examples from functional programming are operations on lists such as map and fold. In mathematics we find functionals in analysis, e.g.,

The order of a functional describes at what level it lives:

In general, the order of a functional is the maximum level of nesting of arrows in its type, where we only count nesting on the right of an arrow. So we have:

In general, functionals over type `t` are those whose types can be generated from `t` by forming functions and functionals of arbitrary order. Real functionals are functionals over the real numbers. There are actually several kinds of functionals:

If you would like to read more about functionals, I recommend John Longley’s comprehensive survey “Notions of computability at higher types” (part 1, part 2, part 3).

Interesting functionals

Now here is a curious thing: it is hard to think of interesting functionals of order 3, and impossible to find interesting examples at level 4. Let me make this claim more precise.

Let us say that a functional is interesting if it is not expressible from lower-order functionals and `lambda`-calculus.

Order 1. At order 1 anything that is not the identity or the constant function is interesting.

Order 2. __Interesting examples of order 2 functionals are not hard to get by:

A functional of order 2 which does not count as interesting is evaluation of a functon at an argument because it can be defined as `lambda f. lambda x. f x`.

Order 3. Now we have to think a little. If we take functional programming to be `lambda`-calculus with recursion, then the recursion operators at every type count as interesting, although I would prefer not to count them as they essentially only use order 2 features to compute fixed points. A better example of a genuinely interesting order 3 functional in functional programming is Martín Escardó‘s program max for computing the maximum of a binary function on Cantor space, which has type `((NN -> 2) -> 2) -> 2` where `2 = {0,1}` are the boolean values, see Section 13.2. of his “Synthetic topology of data types and classical spaces“. We can think of type `NN -> 2` as the type of infinite binary sequences. Input to max is a boolean predicate `p` on binary sequences. The return value is `1` if there exists a binary sequence `a` such that `p(a)=1` and is `0` if `p(a)=0` for all sequences `a`. Before you look at Martin’s program, try defining it Haskell yourself.

An example of functional of order 3 in mathematics is a solution operator which takes a linear differential operator `Phi` and solves the differential equation `Phi(f) = 0`. It could be argued that this is cheating, since `Phi` is usually expressed as `Phi = p(D)` where `D` is the derivative operator and `p` is a polynomial. Thus, the input to `Phi` is actually the polynomial `p`, which is of order 1.

A better candidate for order 3 in mathematics is Feynman’s path integral which takes as input a functional `F` which maps paths (functions) to numbers and computes the “integral” `int F(f) df`, with `f` ranging over all allowable paths. The pedantic readers will be quick to point out that the naive Feynman path integral does not exist, so we would actually want to consider something like Wiener integral instead.

Order 4. Here I am completely lost. If you know of genuinly interesting functionals of order 4, please let me know. I would prefer examples which are total and continuous, and if possible such that they have no counterpart at lower orders. Mind you, it won’t do to just assemble together functionals of lower orders. For an interesting order 4 functional, you would need to say something insightful about order 3. You may look at functional programming, or maybe at functional analysis to get some good candidates. But there do not seem to be any.

I should mention that there is an artificial and unilluminating way of bumping up the order by one. If we view real numbers as Cauchy sequences of rational numbers, each real number appears as an order 1 function on rationals. Thus, automatically any functional of order `n` over the reals is a functional of order `n+1` over the rational numbers.

I mentioned that not much is known about functionals at higher types. To illustrate this, let us consider what we know about continuous functionals over the natural numbers `NN`:

Dag Normann has spent a considerable amount of time thinking about higher-order total continuous functionals over the natural and the real numbers. He has shown that spaces of functionals over natural numbers may be embedded in spaces of functionals over reals. To appreciate this, try embedding `(NN -> NN) -> NN` inside `(RR -> RR) -> RR` (where we only take continuous functionals and equip spaces with sequential topologies).

I might have left you with the impression that functionals of higher order which are definable by `lambda`-calculus are not interesting at all. This is far from truth. Paul Taylor developed a formulation of topology, called Abstract Stone Duality, in which he uses some mind-boggling `lambda`-calculus of order 4 and higher to express topological notions. I suspect Haskell programmers would have an easier time understanding it than classical topologists. Mathematicians are not used to such stuff.

If we count the order of an axiom as its order under propositions-as-types translation, we discover that most axioms in mathematics go up only to order 2? For example, completness of real numbers (“every Cauchy sequence has a limit”) is an order 2 axiom. An axiom of order 3 is Pierce’s law `((P=>Q)=>P)=>P`. What about an axiom of order 4?

My point is this: understanding every next level of functionals requires new concepts and fresh ideas. We have not come very far, as we seem to be stuck mostly at order 2.

Comments

Speaking of Haskell and higher order functions, we might as well mention Chris Okasaki's

Even Higher-Order Functions for Parsing or Why Would Anyone Ever Want To Use a Sixth-Order Function?

http://citeseer.ist.psu.edu/okasaki99functional.html

I was just playing around with a function of order 5, and saw this blog post, so I thought I'd comment.

Call-with-current-continuation in a language with first class continuations (making the type system correspond to classical logic) has type ((p -> q) -> p) -> p, and so is order 3. However, without first class continuations, this type becomes uninhabited.

The natural analogue of call/cc when you don't have first class continuations has type: ((((p -> k) -> k) -> ((q -> k) -> k)) -> ((p -> k) -> k)) -> ((p -> k) -> k) making it order 5. The translation from classical to intuitionist logic increases the order by 2. I think it's reasonable enough to conclude that it's important, given that one form of it is distributed with most Haskell implementations as Control.Monad.Cont.callCC, in the instance of MonadCont for the type Cont k. Whether this qualifies as something having an analogue at a lower order is an interesting question. In order to lower the order of the function to make it more comprehensible, the libraries introduce the type constructor Cont, such that Cont k a is isomorphic to ((a -> k) -> k), which brings the order back down to 3. (Cont k) is then made a monad instance, and callCC is implemented for it in the instance of MonadCont. The implementation needs to actually use the structure of the type of course, making it 5th order, at least in terms of how you have to look at it during implementation.

I would count "adding up" Pierce's Law and continuations to order 5 as cheating. It's not telling us anything more than just the sum of the two concepts we put together.

Post a comment:
Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.

Name

E-mail

Website

Comment