Why can Lambda Calculus not represent some combinators?

Question

This paper suggests that there are combinators (representing symbolic computations) that can not be represented by the Lambda calculus (if I understand things correctly):

Answer 1

There are several things that one may want to do in practice and that cannot be directly expressed in the lambda calculus.

The SF calculus is an example. Its expressive power is not news; the interesting part of the paper (not shown in the slides) is the category theory behind it. The SF calculus is analogous to a lisp implementation where you allow functions to inspect the representation of their argument — so you can write things like (print (lambda (x) (+ x 2))) ​⟹ "(lambda (x) (+ x 2))".

Another important example is Plotkin's parallel or. Intuitively speaking, there's a general result that states that lambda calculus is sequential: a function that takes two arguments must pick one to evaluate first. It's impossible to write a lambda term or such that (or ⊤ ⊥) ⟹ ⊤, (or ⊥ ⊤) ⟹ ⊤ and or ⊥ ⊥ ⟹ ⊥ (where ⊥ is a non-terminating term and ⊤ is a terminating term). This is known as “parallel or” because a parallel implementation could make one step of each reduction and stop whenever one of the argument terminates.

Yet another thing you can't do in the lambda calculus is input/output. You'd have to add extra primitives for it.

Of course, all these examples can be represented in the lambda calculus by adding one level of indirection, essentially representing lambda terms as data. But then the model becomes less interesting — you lose the relationship between functions in the modeled language and lambda abstractions.

Answer 2

The answer to your question depends on how you define "computations" and "represented". The thread on LtU that sclv mentioned, on the other hand, consists mostly of people talking past each other due to misaligned definitions of various terms.

The distinction is certainly not one of computational power--every system under consideration is Turing-equivalent. At issue is that mere Turing-equivalence doesn't really say anything about the structure or semantics of an expression. For that matter, in extremely minimalist models of computation that require complex encodings or non-trivial initial states, it may even be unclear whether a system is capable of universal computation, or whether an illusion of universality is being created by someone's interpretation of the system. For instance, see this mailing list discussion regarding a 2-state, 3-symbol Turing machine, particularly the concerns raised by Vaughan Pratt.

At any rate, the distinction drawn is between something like:

• Things that can be represented directly in a system, by assigning semantics to the primitive operations in such a way that the operations necessarily preserve the semantics
• Things that can be represented "indirectly", by specifying an interpretation procedure performed outside of the system, where the interpretation is assumed to be "simpler" than the system in some sense
• Things that can be simulated in a system by a complete layer of indirection, such as by constructing an interpreter for a different system that provides a direct representation.

Turing-equivalence only implies that a system meets the third criterion for any computable function, whereas it is most often the first criterion that we care about, in either a formal system of logic or a programming language (to whatever extent those actually differ).

That's a very informal description, but the essential idea can be nailed down more precisely. In the aforementioned LtU thread can be found a couple references to existing work along similar lines.

---

Both Schönfinkel's combinatory logic and Church's λ-calculus were initially devised as distilled abstractions of logical reasoning, and as such, their structure maps very neatly onto logical reasoning and vice versa. They also carry an assumption of extensionality, such as described by the eta-reduction rule: λx. f x, where x does not occur in f, is equivalent to just f alone.

In practice, a very strict notion of extensionality can be too limiting, while unrestrained intensionality makes local reasoning about sub-expressions difficult or impossible.

The SF-calculus is a modified combinator calculus that provides, as a primitive operation, a limited form of intensional analysis: The ability to deconstruct partially-applied expressions, but not primitive values or non-normalized expressions. This happens to map nicely onto ideas like pattern matching as found in ML-style programming languages or macros as found in Lisps, but cannot be described in SK- or λ-calculus without, effectively, implementing an interpreter for evaluating "intensional" terms.

So, in summary: The SF-calculus cannot be represented directly in λ-calculus in the sense that the best representation possible most likely involves implementing an SF-calculus interpreter, and the reason for this is a fundamental semantic difference: Do expressions have internal structure, or are they defined purely by their external behavior?

Answer 3

Barry Jay's SF calculus is able to look into the structure of terms it is applied to, which is non-functional. Lambda calculus and traditional combinatory logic are purely functional, and so cannot do this.

There are many extensions of the lambda-calculus that do things that violate purity, most of which require fixing the rewrite strategy to some degree, such as adding state, controls (e.g, via continuations), or logic variables.