The syntax generates strings like
**ii*ii, but not
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.,
((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))))))
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 == SThis 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.
*i*i*iidenotes K. Similarly, if you evaluate the Iota code corresponding to S by inserting
*iat 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.
```sii``sii; in the lambda calculus, similar in behavior to (^x.xx)(^x.xx)). When executed in the Scheme reference implementation (on my system,
S(SK)(SK)(SII)in CL, and of
```s`sk`sk``siiin Unlambda; similar in behavior to the lambda expression
Here are the corresponding infinite-loop programs in Jot (also, try
11100 or S =