Lambda the Ultimate

Notice that one man's program can be another's data.

When I write a program in emacs, the program is data. When I compile it, the program is again data (for the compiler). The resulting object code is data for the loader. The object code in memory, when executed, is "program", but may still serve as data for a debugger.

Things are even more fun when you think about virtual machines (like the Java JVM). The JVM is executing your compiled Java program, so the class file is a program. But if you examine the JVM itself, you notice that treats the class files as data (read from file and interpreted).

These cases are not special cases. The same goes for HTML in the browser (code) and in the validator (data) etc.

You may wonder whether it is possible to answer the original question, when considering pairs of (program,data), instead of single values. For example (browser,html file) will return "program" where as (editor, html file) will return "data". This is also not possible in general, but I'll leave the explanation for another time (essentially, this approach requires you know what the program "does", and this is undecidable).

Remarkably, a type system can ensure that all program[s] terminate, but cannot ensure that all programs written in a Turing complete language not encounter divide by zero problems.

I am curious about this statement (and still very new to programming language theory). I looked in a few online PL textbooks but didn't find this proposition discussed. Can a type system for a "useful" language be devised that ensures all programs written in the language terminate? If I can do something "useful", like find the root of a function with Newton's method, does this mean that the type checker will itself prove the necessary Newton convergence theorems? Since the convergence of Newton's method depends on the properties of the function whose roots are sought, does this mean that the function must be supplied at compile-time (furthering the ambiguity between program and data)?

The possibility of self reproducing automata is quite amazing. By showing the self reproducing automata exist we can convince oursleves that self reproduction (or replication), a major feature of biological life, can be mechanized, and its computational properties studied.

Johnny von Neumann studied this question in the late 1940s (before the discovery of DNA!) His Theory of self-reproducing automata is a tour de-force.

A noteworthy feature of von Neumann's model of self replication is the double-faceted use of the information that serves as the blueprint: It first serves as instructions to be interpreted so as to construct a new universal constructor, after which this same blueprint is copied unmodified, to be atached to the new offspring constructor - so that it may replicate in its turn.

For more information about self-replication research and von Neumann's seminal work read Moshe Sipper, Fifty years of research on self-replication: An overview, Artificial Life, vol. 4, no. 3, pp. 237-257, Summer 1998.

Does anyone really argue against this?

Note that proving program termination is in general also undecidable, except in highly impoverished type systems (e.g. simply typed lambda calculus).

I am curious about this statement (and still very new to programming language theory). I looked in a few online PL textbooks but didn't find this proposition discussed. Can a type system for a "useful" language be devised that ensures all programs written in the language terminate?

Yes, for example Charity. Dependent type systems are another approach, but I don't think they're realistic.

If I can do something "useful", like find the root of a function with Newton's method, does this mean that the type checker will itself prove the necessary Newton convergence theorems?

It is more like you are proving convergence, and the proof you write is executable. The typechecker's role is to ensure that the code you write is a proof; it won't magically come up with a convergence proof for you.

Since the convergence of Newton's method depends on the properties of the function whose roots are sought, does this mean that the function must be supplied at compile-time (furthering the ambiguity between program and data)?

No.

If termination depends on the properties of a function, then in a Charity-like language you will need to come up with an inductive datatype for representing functions because termination is ensured by structural induction. This means you will need to define a little language of terms which denote functions and compute the necessary properties by recursing over them in a particular manner.

In this case, the functions are functions on reals, though, and I am pretty positive you will not be able to define such a datatype in Charity. Your only hope for coding up Newton's method in Charity would be to figure out a way of generalizing it to a more discrete domain.

In a dependently typed language, it would be possible (in a dependently typed language anything is possible), but you would undoubtedly need a huge library encoding information about Dedekind or Cauchy reals, real analysis, etc. Coding up such stuff is difficult enough; making it efficient would be a vast undertaking.