|
The syntax generates strings like i, *ii,
*i*ii, or **ii*ii, but not ii,
i*i, or **ii.
The semantics is expressed using the lambda calculus. The symbol
"^" stands for lambda, and the functions S and K are the standard
functions from Combinatory Logic (henceforth referred to as "CL"): S =
^xyz.xz(yz) and K = ^xy.x. If you're not
familiar with CL, see, e.g., Hankin's 1994 Oxford book, Lambda
Calculi: A guide for computer scientists, or the wonderful
Unlambda page for a thorough explanation. Note that as usual,
functional application is left-associative, so that, e.g.,
xSK = ((x(S))(K)). The expression
[F] indicates "the meaning of the expression F"; in other
words, the star prefix in the syntax corresponds to functional
application in the semantics.
Iota is highly similar to other simple Turing-complete languages.
For one thing, the trick of using the star prefix instead of left and
right parentheses is a strategy also adopted in Unlambda. (In fact,
in general, exploring the
Unlambda page will help tremendously in understanding this
document.) For another, Hankin (page 61) proposes the term
^x.xKSK as a one-element basis for the lambda-calculus;
my language pursues essentially the same idea, except that my unique
basis element is marginally simpler (^x.xSK instead of
^x.xKSK). Of course, when there is only one element in
the basis, even a marginal difference in simplicity is a substantial
fraction of the whole!
18 March 2002: Jeroen Fokker compares a number of one-combinator bases. He claims that his (^f.fS(^x^y^z.x)) is the smallest, but does not consider my combinator. For purposes of comparison, my combinator can be rendered as ^f.fS(^x^y.x), which is clearly smaller. Fokker is trying to minimize the number of combinators it takes to reconsruct K and S, and on that score, he wins (2 and 3, respectively, for him versus 4 and 5 for me--see below). But in terms of the size of the combinator itself, I win. See Fokker 1992, `The systematic construction of a one-combinator basis for Lambda-terms', Formal Aspects of Computing 4:776-780, available here .
Here is a complete reference implementation for Iota in R5RS Scheme:
(let iota ()
(if (eq? #\* (read-char)) ((iota)(iota))
(lambda (c) ((c (lambda (x) (lambda (y) (lambda (z) ((x z)(y z))))))
(lambda (x) (lambda (y) x))))))
*".) If you want to try out Iota,
you can either download the reference interpreter and run it in a
Scheme interpreter, or try the JavaScript program below.
Why care whether Iota is unambiguous?
If ambiguous languages were allowed, we could do without the star, and
have an even simpler language:
Syntax Semantics
F --> i ^x.xSK
F --> F F [F][F]
To prove that Iota is Turing-complete, I will provide a mapping from Combinatory Logic into Iota that preserves meaning; since CL is Turing-complete, Iota is too. The mapping goes like this:
CL Iota
I ==> *ii
K ==> *i*i*ii
S ==> *i*i*i*ii
AB ==> *[A][B]
Since the expression "*[A][B]" in Iota means the same thing as
"AB" in CL (namely, functional application in which the meaning of A
is applied as a function to the meaning of B), we need only establish
the appropriateness of the translations of the lexical items I, K, and
S. Bear in mind that functional application is left-associative:
*ii
== (^x.xSK)(^x.xSK)
== (^x.xSK)SK
== SSKK
== SK(KK)
== I
*i*i*ii
== i(i(ii))
== (^x.xSK)((^x.xSK)((^x.xSK)(^x.xSK)))
== (^x.xSK)((^x.xSK)I)
== (^x.xSK)(ISK)
== (^x.xSK)(SK)
== SKSK
== KK(SK)
== K
*i*i*i*ii
== i(i(i(ii)))
== (^x.xSK)K
== KSK
== S
This establishes that for every expression in CL, there is an
expression in Iota with the same meaning.
In addition, it is easy to find a meaning-preserving mapping from Iota into CL: the semantics in the definition for Iota are given as a mapping from Iota to the lambda calculus, and there are well-known techniques for mapping the lambda calculus into CL (see, e.g., Hankin or the Unlambda page for details).
Goedel's famous incompleteness theorem depends on finding a way to map the natural numbers onto the set of effectively computable functions. Such so-called Goedel numberings are usually fairly complex, and typically involve factoring the number in certain clever ways and mapping the result onto a string of symbols in a formal language. The techniques used to construct Iota give rise to a similar but distinct language that I will call Jot. One of Jot's interesting properties is that it provides a particularly elegant Goedel numbering.
In many ways, Jot is simpler than Iota, though it is slightly more complex to describe:
|
One interesting difference between Iota and Jot is that in Iota, the parentheses operator, *, was treated syncategorematically. In Jot, 1 serves the same purpose, but it is treated lexically. In other words, in Iota, * is a punctuation mark, but in Jot, 1 denotes a function just like i in Iota or 0 in Jot.
Unlike Iota, where the syntactic tree for a string can branch either on the left or on the right, Jot syntax is uniformly left-branching. As a result, Iota is strictly context-free, but Jot is a regular language.
The reference implementation of Jot requires one extra line, because it is necessary to check for end of file in order to know when the expression is finished:
(let jot ((v (lambda (x) x)))
(cond ((eof-object? (peek-char)) v)
((eq? #\1 (read-char)) (jot (lambda (f) (lambda (a) (v (f a))))))
(else (jot ((v (lambda (x) (lambda (y) (lambda (z) ((x z)(y z))))))
(lambda (x) (lambda (y) x)))))))
The semantics of Jot are similar to those of Iota, but not identical. For one thing, the 1 operator does not treat 0 as a unit, but is capable of dividing the meaning of 0 into its K half and its S half. As a result, there are typically more 1's than 0's in a useful Jot program, in comparison with Iota, in which there must always be exactly one more i than there are *'s in order for the expression to be well-formed.
Here are the rules for mapping an arbitrary CL program into Jot:
CL Jot
K ==> 11100
S ==> 11111000
AB ==> 1[A][B]
Note that every CL expression translates into a Jot expression that
begins with 1.
Constructing a Goedel-numbering now becomes trivial: simply express each natural number in base 2 as a string of 1's and 0's. Since every such string is a legitimate Jot program, each base-2 numeral will give rise to a legitimate Jot program. Furthermore, since the base 2 representation of a number always begins with a 1, and since the translation of each CL expression begins with a 1, for every CL program there will be a numeral with the same interpretation. Since CL is Turing-complete, we have a suitable Goedel-numbering in which the base-2 representation of the number itself is treated as a program directly.
In order to make it convenient to try out Iota and Jot, I have embedded interpreters within this web page, coded in JavaScript. (You must have JavaScript turned on in your browser for this to work.) You can look at the JavaScript code by clicking on View->Page Source. The interpreter is designed to pop up an "alert" window, which trys to present the function denoted by the Iota program.
*i*i*ii
denotes K. Similarly, if you evaluate the Iota code corresponding to
S by inserting *i at the beginning of the program to make
it *i*i*i*ii, clicking should produce an alert window
containing code for S.In general, however, since the alert window does not provide full access to the closure denoted by the Iota program, examining the alert window is not terribly helpful. And since Iota (unlike most practical programming languages) does not produce any output, it can be difficult to verify that the program is behaving as expected.
Nevertheless, it is possible to observe indirectly whether the interpreter is working as it is supposed to. For instance, consider what ought to happen when the program denotes an infinite loop: the interpreter will either run forever, or run out of resources. Unfortunately, there is a price to pay for the convenience of running the interpreter inside of a browser: JavaScript interpreters are usually designed to fail silently. But most browsers provide a JavaScript console that will tell you when a stack overflow occurs. You can open the console by clicking on Task->Tools->JavaScript console or some such. Warning: running these infinite loops may cause some browsers to crash---on my system, Netscape 4.77 crashes.
(SII)(SII) (in Unlambda,
```sii``sii; in the lambda calculus, similar in behavior
to (^x.xx)(^x.xx)). When executed in the Scheme reference
implementation (on my system, echo -n
'****i*i*i*ii*ii*ii***i*i*i*ii*ii*ii' | guile -l iota.scm), my
Scheme interpreter loops (apparently) endlessly. Using the JavaScript
interpreter provided by my browser, there are two symptoms that the
expression does indeed correspond to an infinite loop: the interpreter
does not return any value at all, and I get the error message "too
much recursion" in the JavaScript console.S(SK)(SK)(SII) in CL, and of
```s`sk`sk``sii in Unlambda; similar in behavior to
the lambda expression
(^x.xx)(^x.x(xx)).) On my Scheme interpreter, the behavior is
different than the last example; rather than looping endlessly, it
causes a stack overflow. On the JavaScript interpreter, however, it
causes "too much recursion", just like the first example.Here are the corresponding infinite-loop programs in Jot (also, try
K = 11100 or S = 11111000):