We want to show that a conventional machine model can be simulated in the λ-calculus with only a constant amount of overhead.
Choice of Machine Model.
The most realistic choice would be a RAM. However, there are several vari-ants differing in their basic instruction sets and their complexity measures.
It seems that the idea of a “unit-cost” RAM is flawed from a theoretical standpoint, unless its arithmetic instruction set is restricted to contain only the successor function, and no shift operations are permitted (see [Sch80] for discussion and references). An alternative is the “logarithmic cost” RAM.
However, this model also seems flawed in that it seems unable to read and store its input in linear time (see [Sch88] for details).
The Turing Machine (TM) is a more basic model, for which the choice of a basic instruction set does not influence the complexity measure. However, the TM is unrealistically slow, because its storage tapes only allow sequential access. Sch¨onhages Storage Modification Machine overcomes this deficiency, but seems too powerful for our purposes. (See [HBTCS, ch.1] for a presen-tation and discussion of all these models).
We introduce a strengthed version of the TM. Our version uses trees rather than tapes as a storage medium. The tree TM has a complexity measure that is closely related to the RAM measures. Yet, the tree TM has the same simple instruction set as the conventional TM with tape storage.
Definition A.1
k-tree Turing Machine
A k-tree Turing machine consists of two i/o tapes, k work-trees and a finite control. The input tape contains initially a string over{0,1}terminated by a
’#’ and one head positioned at the left end of the tape. The head may read symbols and move to the right (and nothing else). The output tape is initially empty and has one head positioned at the left end of the tape. The head may
write symbols {0,1,#} and move to the right, but nothing else. Both trees are initially empty, i.e. all cells contain the blank symbol, and each tree has one head that may both read and write in addition to moving stepwise in one of the directions{1,2,3}. In each step, ak-tree Turing machine reads the cell symbol under each of the (k+ 1) heads that are allowed to read, inspects the state, and based upon the transition function, the control changes the state, overwrites the symbol under each of the the (k+ 1) heads that are allowed to write and moves some (or none) of the (k+ 2) heads in legal directions.
A k-tree Turing machine M is said to compute a function f : {0,1}n → {0,1}m whenever the following holds:
For all (a1, a2, ..., an) in {0,1}n, we have f(a1, a2, ..., an) = (b1, b2, ..., bm) if and only if M started on an input tape ’a1, a2, ..., an,#’ stops with output tape ’b1, b2, ..., bm,#’.
The complexityTM(n) of the machine M is the maximum number of steps taken before halting on any input of length n. The size of a k-tree Turing Machine with q states and s symbols isq·sk·log(q·sk).
It should be clear to the reader that the complexity measure defined by the k-tree TM is very close to that defined by the various RAM models.
More or less all the models discussed above define complexities that differ by at most a log factor. Informally, a k-tree TM may be used to simulate a RAM by using one of its trees to simulate the RAM’s memory with binary addressing in the intuitive way. A second tree may be used to assist with bookkeeping and arithmetic instructions. Thus a similar complexity measure to the logarithmic cost RAM is obtained, but at much greater simplicity. The reasons for our choice of the k-tree TM will become apparent.
Definition A.2
Control and data structures encoded as λ-expressions We give specific names to some very usefulλ-expressions:
• The truth-values:
t = (λxy.x) f = (λxy.y)
These are conveniently used for a conditional control expression if cthen L else N fi
to be coded as
(cLN)
We may also encode an iterative (recursive) control expression P l0
where
P L=if (cL) then (P(pL))else (qL) fi using the least fixed point combinator Y from definition 1:
P =Y(λf.λL.(cL)(f(pL))(qL))
• The data structure list
[ ] = (λx.I)
[M0, M1, . . . , Mn] = (λx.xM0[M1, . . . , Mn]) with the indexing functions
tln = (λx.xff. . .f) hdn = (λx.(tlnx)t)
where the defining expression for tln containsn copies of f and tlk[M0, M1, ..., Mn] = [Mk, ..., Mn]
hdk[M0, M1, ..., Mn] = [Mk]
• Unary integers.
un=hdn
Definition A.3
λ-programs
Let f : {0,1}∗ → {0,1}∗ be a partial function on Boolean strings. A λ-expression N computes f when
1. iff(b1, ..., bn) = (c1, ..., cm) thenL= (N[ub1, ..., ubn, u2]) has the normal form [uc1, ..., ucm, u2].
2. if f(b1, ..., bn) is undefined then Lhas no normal form.
Proposition A.4
Efficient simulation of tree Turing Machines in the λ-calculus For every 2-tree TM M there is a λ-expression N and a constant c such that N and M compute identical functions and if M on input (b1, ..., bn) halts aftertsteps then theλ-expressionL= (N[ub1, ..., ubn, u2]) satisfies that µπ(L) =µβ(L) = lnormal(L)≤c·t.
Proof
For a given 2-tree Turing Machine M we construct aλ-program as follows.
Both symbols and states are represented by unary numbers such that for symbols
1. u0 and u1 denote the bit-symbols 0 and 1.
2. u2 denote the tape end-marker #.
3. u3 denotes the blank symbol.
and for states
1. u0 denotes the initial state.
2. u1 denotes the unique halt state.
An instantaneous description of the 2-tree Turing Machine is kept as a list of five elements
id= [state,tree1,tree2,tapei,tapeo]
One may regard a tree as having a root at the head position and being directed away from this root, in which case each node in the tree has two outgoing edges and one incoming edge except for the root that has three outgoing edges and no incoming edges. Every subtree may be represented as the symbol at the subtree-root combined with a subtree for each edge that goes out of the root. For simplicity, we take a subtree for each incident edge:
tree= [t,symbol,tree1,tree2,tree3]
where in the case of an incoming edge, the corresponding tree is empty, represented by
treee = [f, u3]
The empty tree is also used as a representation of unexplored subtrees that have blank symbols at all nodes. The truth-value occurring as the first element in the list representation of a tree is used to distinguish the empty tree.
A tape is represented by a recursive list
tape= [symbol,tape]
that may be empty
tapee = [u2]
Too see how a single step of a computation on the 2-tree Turing Machine may be simulated, we look at a representative example. Assume that in the current id, we must make the following changes
1. The finite state control goes into state.
2. symbol1 is written under the head of tree1, which stays.
3. symbol2 is written under the head of tree2, which moves one step in direction 1.
4. The head of the input tape is moved one step (necessarily to the right).
5. symbol is written on the output tape (and the head is moved one step to the right).
The following λ-expression will applied to an id reduce to a modified id as prescribed above.
(λx.[ state,
[t, symbol1, tl2(hd1x)],
[ t,
hd1(hd2(hd2x)),
[t, symbol2, treee, tl3(hd2x)],
hd0(hd2(hd2x))tl3(hd2(hd2x)) [treee, treee] ]
tl1(hd3x), [symbol, hd4x]
])
The most complicated part of the above expression is the modification of tree2. It is here necessary to provide two alternative sub-actions according to whether the subtree in direction 1 has been visited before or not. The choice is made by the truth-valued expression hd0(hd2(hd2x)).
The state and symbols under the heads in the presentiddetermines which action to take. All possible actions are therefore organised in a 4-dimensional array transitiontablethat is indexed by
1. state
2. symbol under head of tree1
3. symbol under head of tree2
4. symbol under input head
The simulation of one single transition step may thus be done by the following λ-expression that updates its argument (an id) appropriately:
F = (λx.hd0(tl3x)(hd1(tl2x)(hd1(tl1x)(hd0x transitiontable)))x) We are now in a position to describe the whole simulation. For control purposes we define a constant expression
halt= [f,t,f,f, . . . ,f]
with the property that ’ui halt’ reduces to t precisely when ui denotes the halt state (The size of the expression for halt is proportional to the num-ber of states in the machine M). Assume the λ-program G on argument id reduces to the output tape eventually computed if id leads to a halting configuration, and otherwise G does not reduce to a normal form. This G may be characterised recursively: G= (λx.hd0x halt(hd4x)(G(F x))), i.e. if the present configuration contains a halt state then the result consists in the present output tape (hd4x), otherwise apply G to the result of yet another iteration, G(F x). HenceG may be defined by
G=Y(λg.λx.hd0x halt (hd4x) (g(F x))).
G gives the output tape in reverse order, and then we need a list reversal function. Define first the constant expression
end= [f,f,t,f,f, . . . ,f]
with the property that ’ui end’ reduces to t precisely when ui denotes the tape end marker #. The reversal function is
Rev = (λz.Y(λh.λx.λy.hd0y end x (h[hd0y, x](tl1y))) [u2]z) i.e. Rev[ui1, ui2, . . . , uin, u2] reduces to [uin, uin−1, . . . , ui1, u2] whereij = 2.
Define
id0 = (λx.[u0,[t, u3, treee, treee, treee],[t, u3, treee, treee, treee], x,[u2]]) which applied to an input tape [ub0, . . . , ubn, u2] reduce to the initialidof the 2-tree Turing Machine. Finally define the λ-program
N = (λx.Rev(G(id0x)))
that computes the same function as the 2-tree Turing Machine M does.
It should be clear from the construction that the number of β-reduction steps needed for the simulation of a single TM-step is bounded by a constant.
We find also that regular β-reduction in any order is as efficient as normal order parallel reduction, essentially because a list indexing function forces an order of reduction by creating only one redex at a given time. Where more than one indexing function is enabled the corresponding reduction steps are independent and may be done in any order. Hence µπ(L) = µβ(L) = lnormal(L).
QED.
References
[Bar81] Barendregt, H. P.,The Lambda Calculus. Its Syntax and Seman-tics.North Holland, 1981.
[Bur82] Burton, F. W., A Linear Space Translation of Functional Pro-grams to Turner Combinators. Information Processing Letters, 14 (1982), pp. 201-204.
[deB72] de Bruijn, N. G., Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation. Indag Math, 34 (1972), pp. 381-392.
[Chu32] Church, A., A Set of Postulates for the Foundation of Logic.
Annals of Math. 33, 2nd series (1932), pp. 346-366.
[CuFe58] Curry, H. B. and Feys, R. Combinatory Logic, Vol. 1. North Holland, 1958.
[Fie90] Field, J., On Laziness and Optimality in Lambda Interpreters:
Tools for Specification and Analysis. In [PoPL90], pp. 1-15.
[HBTCS] the Handbook of Theoretical Computer Science, vol A(ed. J. van Leeuwen). Elsevier, Amsterdam, 1990.
[Hug82] Hughes, R. J. M., Super Combinators: A New Implementation Method for Applicative Languages. In Proceedings of the 1982 ACM Symposium on Lisp and Functional Programming, pp.1-10.
[Hug84] Hughes, R. J. M.,The Design and Implementation of Programm-ing Languages.Ph.D. Thesis, Oxford University, 1984. (PRG-40) [KeSl87] Kennaway, J. R. and Sleep, M. R., Variable Abstraction in O(nlog(n)) Space. Information Processing Letters, 24 (1987), pp. 343-349.
[Klo80] Klop, J. W., Combinatory Reduction Systems. Mathematical Centre Tracts 127. Mathematisch Centrum, Amsterdam, 1980.
[Lam90] Lamping, J., An Algorithm for Optimal Lambda Calculus Re-duction. In [PoPL90], pp. 16-30.
[L´ev80] L´evy, Jean-Jacques, Optimal Reductions in the Lambda-Calculus. In Seldon, J. P. and Hindley, J. R. (editors), To H.
B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism,Academic Press, 1980, pp. 159-191.
[L´ev88] L´evy, Jean-Jacques, Sharing in the Evaluation of Lambda Expressions. In Fuchi,K. and Kott,L. (editors),Programming of Future Generation Computers II,North Holland, 1988, pp. 183-189.
[Nos85] Noshita, K., Translation of Turner Combinators in O(nlog(n)) Space.Information Processing Letters, 20 (1985), pp. 71-74.
[PoPL90] Proceedings of Seventeenth Annual ACM Symposium on Prin-ciples of Programming Languages. ACM, New York, 1990.
[R´ev88] R´ev´esz, G. E., Lambda-Calculus, Combinators and Functional Programming. Cambridge University Press, 1988.
[Ros84] Rosser, J. B., Highlights of the History of the Lambda-Calculus.
Annals of the History of Computing 6 (1984), pp. 337-349.
[Sch24] Sch¨onfinkel, M., ¨Uber die Bausteine der mathematischen Logik.
Matematische Annalen, 92 (1924), pp. 305-316.
[Sch80] Sch¨onhage, A., Storage Modification Machines. SIAM Journal on Computing 9 (1980), pp. 490-508.
[Sch88] Sch¨onhage, A., A Nonlinear Lower Bound for Random-Access Machines under Logarithmic Cost. Journal of the ACM 35 (1988), pp. 748-754.
[Sta82] Staples, J., Two-Level Expression Representation for Faster Eva-luation. In Ehrig,H., Nagl,M. and Rozenberg,G. (editors), Proce-edings from 2nd International workshop “Graph Grammars and their Application to Computer Science”.Springer Verlag (LNCS 153), 1983, pp. 392-404.
[Tur79a] Turner, D. A., Another Algorithm for Bracket Abstraction.The Journal of Symbolic Logic 44 (1979), pp. 267-270.
[Tur79b] Turner, D. A., New Implementation Techniques for Applicative Languages. Software: Practice & Experience. 9 (1979), pp. 31-49.