Lambda the Ultimate

From the top of my head I can suggest several:

1. Cognitive factors. While it could be possible to express the same functionality in most languages, the feel of the code may be radically different, in extreme cases resulting in unbearable strain.
2. Software engineering factors (can be merged with 1). The goal is not only to provide a code for the functionality, but to debug, maintain, and evolve it.
3. Non-batch functionality. Turing completeness is oriented towards functions from input to output, while more or less ignoring interaction, time, trust, fairness.

Is this topic worth a discussion?

I thought this WAS the discussion here at LtU. ;-)

Seriously, though, don't we all take if for granted that (except maybe for some interesting corner-cases) a PL will be Turing complete?

The whole of what we discuss here seems to be "Given Turing completeness, what other factors of PL design are significant and how?"

Cognitive factors, Software engineering factors, etc

As many here will know ;-), I strongly believe that "human" factors are fundamental to PL design and effectiveness. Unfortunately, they are also very hard to study in a satisfactory, i.e. well-defined and objective, way.

1. Cognitive factors. While it could be possible to express the same functionality in most languages, the feel of the code may be radically different, in extreme cases resulting in unbearable strain.

<groan> No comment. But see below on `broadly interpreting' Turing-completeness.

2. Software engineering factors (can be merged with 1). The goal is not only to provide a code for the functionality, but to debug, maintain, and evolve it.

Right, Turing-completeness does not address this, because it only says anything about the dynamic properties of a language, whereas developing, debugging, optimizing, maintaining, refactoring, etc. are all static activities, things you do with a program rather than in it.

Static typing does address these concerns. This will appear in my article.

3. Non-batch functionality. Turing completeness is oriented towards functions from input to output, while more or less ignoring interaction, time, trust, fairness.

Inasmuch as Turing-completeness deals with Turing machines, it doesn't treat these issues well, since Turing machines don't treat them well.

However, broadly interpreted Turing-completeness doesn't have anything to do with Turing machines, but rather computability itself, and so we are not talking only about a translation to Turing machines, but also anything else, like the untyped lambda-calculus or Milner's pi-calculus, which has the same computational power. (In fact, when you say "functions from input to output above" I think you are already interpreting Turing-completeness broadly, since that sounds more like Church's partial recursive numeric functions than anything to do with tapes and states and configurations.)

Some of these models do treat some of those issues more directly. For example, pi-calculus clearly has something to do with interaction. The equivalence of all these computational models, though, means basically that, even though Turing machines don't explicitly deal with interaction or fairness or whatever, they can be dealt with indirectly by encoding.

Anyway (and I think this is more important) you don't have to abandon the principle of Turing-completeness to deal with interaction, time, whatever. It's not an either-or thing!

BTW, here is an interesting article about `going beyond' Turing-completeness.

Peter Wegner. Interaction, Computability, and Church's Thesis.

Lots more stuff on the same subject at his publications page.

(Actually, I think I've cited one of his articles on this subject here before.)

Or just criticizing the usefulness of Turing-completeness as a concept?

Right. It gives too little (for modern software systems), and is valued too much. I agree that any general-purpose language should be Turing-complete, but this is but one of dozens of checks on the list.

Anyway (and I think this is more important) you don't have to abandon the principle of Turing-completeness to deal with interaction, time, whatever. It's not an either-or thing!

Agree. I don't want to abandon, just to extend.

I thought you will mention pi-calculus, but I didn't see much results on how pi-calculus is more expressive than, say, lambda, therefore proving that pi is above Turing-completeness. (there are a lot of technical results, and I feel that temporal or linear logic are quite expressive, but I mean I want a thesis as bold as that of Church)

Peter Wegner. Interaction, Computability, and Church's Thesis.

Ah, quite interesting. I will have to re-read this tomorrow, it's 11PM here, so I was not able to follow all the points. But looks very much like what I needed, a lot of bold statements and generalisations :-) Thanks!

PS: so now it's Wolfram-completeness <= Turing-completeness <= Wegner-completeness :-)

I seem to recall that regular expressions are not Turing-complete. I guess there are more DSL's that aren't.

As far as more general purpose languages are concerned, wouldn't it not only be a theoretical but also a obvious practical limitation if one wasn't Turing-complete?

No; general recursion breaks the Curry-Howard isomorphism. CH says that you can interpret logical formulas as polymorphic types, and proofs of that formula as functional programs. So "A and B" is interpreted as the pair type constructor, "A or B" is the disjoint sum, implication "A => B" is the function type "A -> B" and so on. However, once you add general recursion -- a letrec statement -- then the isomorphism is no longer true, because you can write programs whose types correspond to false propositions. For example, the formula "forall a, b. a => b" is clearly not true. And yet, if you fire up ML:

# let rec foo x = foo x;;
val foo : 'a -> 'b = <fun>

Quite simply, this is an abomination before the Lord. :) We are kept from eternal damnation only by the slenderest thread of grace: attempts to use false programs to create contradictory values will never terminate. But wouldn't it be awesome if programs really were *genuine* proofs in a constructive logic?

I hope not. I personally find non-turing complete languages are more interesting. There is a ton of important research done on query languages (SQL included) that uses the theoretical tools from the rest of the programming language community, especially recently. Take XQuery, it has marks of the functional programming community all over it.

And AFAIK, you can talk about type systems separately from the terms of the languages they are applied too. So type systems are really executable languages in their own right.

Of course if you use the term PL to specifically mean turing-complete languages, which some people do, then it is true by definition.

AFAIK the best-known non-Turing-complete general-purpose language is Charity.

We discussed Charity on LtU a while back...

I'm not sure where you are coming from here Neel, but it was my understanding that Andris meant the Turing Completeness of the language itself, not necessarily of its type system.

Of course. Completeness is the starting point for a programming language, not the conclusion. The remaining `checks' fall into the categories of static and dynamic expressiveness. It seems that many programmers are unaware of this and think that, since every language is Turing-equivalent and so must be equivalent to every other, it follows that the differences between languages must lie wholly in their syntax.

But this is a logical error. If my notion of equivalence between two things is, `X is round', then I can say a clown nose is equivalent to an egg. But if my notion of equivalence is, `X is red' then they are inequivalent. Furthermore, there are coarse and fine-grained notions of equivalence. `X is round and red' is more fine-grained than `X is round' alone. Turing-equivalence is the coarsest equivalence on programming languages, by definition, because a language is a programming language if and only if it's Turing-complete. More fine-grained equivalences exist, though: `Higher-order functions are definable in X', `First-class continuaions are definable in X', `X is statically typeable', etc. These are semantic questions.

But the stuff Wegner talks about is quite different in character from static and dynamic semantics. It seems to me that he's not really interested in what you can say about programming languages in isolation, but rather what you can say about programming languages in some context, where there is interaction with an outside environment. It's more holistic.

Neel: general recursion breaks the Curry-Howard isomorphism.

This is not really true. A type system with recursion corresponds to an inconsistent logic. The CHI doesn't require that the logic in question has to be consistent; everything CHI claims remains true. Now, of course you can argue, "What is the point of an inconsistent logic?", and to see what the point is you just have to ask yourself, "What is the point of a type system with recursion?" Obviously the latter still has a lot of uses.

The reason for that is that there is more to CHI than types-as-propositions; it also mentions programs-as-proofs. Although an inconsistent logic is kind of degenerate at the propositions level, it is still interesting at the proof level. For example, even though inconisistency implies every proposition has at least one proof, it may still have more than one proof, and the ones that don't use the recursion axiom are still `sensible'. Also cut elimination (proof normalization) still holds.