BRICS RS-95-42 M. Goldberg: An Adequate Left-Associated Binary Numeral System

BRICS

Basic Research in Computer Science

An Adequate Left-Associated Binary Numeral System in the λ-Calculus

Mayer Goldberg

BRICS Report Series RS-95-42 ISSN 0909-0878 August 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

An Adequate

Left-Associated Binary Numeral System in the λ-Calculus ^{∗}

Mayer Goldberg Computer Science Department Indiana University ^{†} (mayer@cs.indiana.edu)

August 15, 1995

Abstract

This paper introduces a sequence of λ-expressions, modelling the binary expansion of integers. We derive expressions computing the test for zero, the successor function, and the predecessor function, thereby showing the sequence to be an adequate numeral system. These functions can be computed efficiently. Their complexity is independent of the order of evaluation.

Keywords: Programming calculi, λ-calculus, functional programming.

∗This work was carried out while visiting BRICS (Basic Research in Computer Science, Centre of the Danish National Research Foundation).

†Bloomington, IN 47405, USA.

1 Introduction

1.1 Numeral Systems in the λ-Calculus

Numbers are traditionally represented on computers with a size proportional to their logarithm. Traditional numeral systems in the λ-calculus, such as Church numerals [1, 3] and Barendregt numerals [1], however, typically involve linear representations of numbers. In such systems, the size of the representation of a number n is proportional to n.

In this paper, we present an adequate binary numeral system for the λcalculus, where the successor function, the predecessor function, and the test for zero are implemented efficiently. This implementation does not depend on the order of evaluation.

Both the particular representation used in this paper and the problem of showing that it is an adequate numeral system are due to H.P. Barendregt. They were given to the author as a challenge during a visit to Indiana University in 1990 [2].

1.2 Prerequisites and Notation

We assume some familiarity with the λ-calculus [1, 3]. The identity combinator is given by I = λx.x. The boolean values true and false are denoted by T = λxy.x and F = λxy.y respectively. Conjunction is denoted by and = (λxy.(x (y T F) F)). Selectors are given by U_{k}^{n} = λx_{0} ⋯ x_{n}.x_{k} where k ≤ n. The ordered n-tuple ⟨x_{1}, …, x_{n}⟩ is denoted by [x_{1}, ⋯, x_{n}] = λs.(s x_{1} ⋯ x_{n}). The k-th projection of an ordered n-tuple is denoted by π_{k}^{n} = λx.(x U_{k−1}^{n−1}). The length of a λ-term M is the number of symbols it occupies, and is noted as ||M||. Finally, the reflexive, transitive closure of the one-step reduction ⟶ is given by ⟶.

2 Binary Numerals

2.1 Representation

Since various data structures can be implemented in the λ-calculus, we could select any one of several different binary representations for our numerals. We choose to use, however, a representation that is unique to the λ-calculus:

2.1.1 Definition: (Barendregt) The Sequence bin = {bin_{n}}_{n∈ω}. We define bin_{n} as follows: Let the variable z (pronounced “zero”) represent a 0-bit, and let the variable w (pronounced: “wan”) represent a 1-bit. Let b_{1}b_{2} ⋯ b_{k}, b_{j} ∈ {z, w}, be a sequence of bits corresponding to the binary expansion of n, such that b_{1} and b_{k} are the low and the high bits respectively. Then

bin_{n} = λzw.(b_{1} ⋯ b_{k})

The sequence of bits is thus represented by a left-associated application of z’s and w’s. 2.1.2 Example:

bin_{0} = λzw.z
bin_{1} = λzw.w
bin_{2} = λzw.(z w)
bin_{3} = λzw.(w w)

bin_{4} = λzw.(z z w)
bin_{5} = λzw.(w z w)
bin_{6} = λzw.(z w w)
bin_{7} = λzw.(w w w)

Our goal in this paper is to show that the sequence bin is an adequate numeral system, and that the successor function, the predecessor function, and the test for zero can all be computed on the bits directly, without expanding their argument into some linear representation. In our Ph.D. thesis [6], we show similarly that addition, subtraction, multiplication, quotient, remainder, and the test for equality can also be computed on the bits directly. These extensions lay beyond the scope of this paper.

2.2 Uniqueness of Representation

One problem affects all n-ary numeral systems: A representation is not unique, that is, different representations exist for the same number. For example, in our system, λzw.w, λzw.(w z z), and λzw.(w z z z z z) all represent the number 1. In the λ-calculus, however, it is extremely inelegant for two numbers to have different normal forms, and yet to be numerically equal.

We thus propose the following two-fold compromise:

• We define the test for zero (and ultimately, the test for equality) to ignore trailing zero bits.

• We define the predecessor function (and ultimately, addition, subtraction, multiplication, quotient, remainder, etc.) not to leave trailing zero bits.

So the functions we provide do not introduce trailing zeros in their results, and ignore them in their arguments. Another solution, which is simpler to derive and to verify, would be to define a “normalisation” combinator, taking a binary numeral and removing its trailing zero bits. This solution, however, is less efficient.

2.3 Size of Our Representation

The size of bin_{n}, our representation of n, is proportional to the number of bits in the binary expansion of n, i.e., to log n. It is also clear that bin numerals are as concise (in the sense of having the least number of symbols) as possible for a binary numeral system in the λ-calculus. What is not as obvious, but just as important if bin is to be practical for implementation on a digital computer, is whether the various arithmetic operations that we might want to carry out on this representation can be computed directly on the bits, without expanding our binary representation to a less compact one. We do not have the benefit, for example, of switching to and from one of the well-known, linear numeral systems in order to define arithmetic functions in one system in terms of the other system, as Barendregt does it in Lemma 6.4.5 and Corollary 6.4.6 of his reference book on the λ-calculus [1, Page 140]. This notion of expansion need not be explicit, but could be implicit in a particular reduction sequence. The following definitions let us express formally just how much can a given expression “expand”: 2.3.1 Definition:

i. Finitely Wide Terms. A λ-term M is finitely wide if there exists a number N > 0, such that if for all λ-terms x, if M ↠_{R} x then ||x|| ≤ N.

ii. The Width of a Term, 𝔴𝔡.^{1} The width of a finitely wide term M, denoted by 𝔴𝔡(M) is given by

𝔴𝔡 = sup{||x|| : M⟶x}

1 𝔴𝔡 is wd in Gothic letters.

The following two points should be noted:

• Some λ-terms which do not have a finite width, but have a normal form. For example, let M be defined as follows:

M = (\underline{(λf.((λx.(f (x x))) (λx.(f (x x)))))} (λxy.y) I)

It is simple to verify that M⟶I. The underlined sub-expression, however, does not have a normal form, and expands arbitrarily. We can thus have reduction sequences that result in expressions of arbitrary width. Therefore M does not have a finite width.

• Some λ-terms do not have a normal form, but have a finite width. For example, let M be defined as follows:

M = ((λx.(x x)) (λx.(x x)))

It is simple to verify that M ⟶ M, and so M has a finite width, but no normal form.

The width of a λ-term is used in the proof that a test for zero, the successor function, and the predecessor function can all be computed without expanding the representation of their arguments beyond log n.

3 Arithmetic Functions

3.1 Testing for Zero

3.1.1 Proposition: There exists a combinator Zero?_{bin} such that for all n ∈ ℕ we have

i.

(Zero?_{bin} bin_{0}) ⟶ T
(Zero?_{bin} bin_{n+1}) ⟶ F

ii. 𝔴𝔡(Zero?_{bin} bin_{n}) = O(log n).

Proof:

i. To compute the zero predicate, we apply a given numeral to two λexpressions, substituting those λ-expressions respectively for z and w, in the body of the numeral. The problem of testing for zero thus reduces to the problem of identifying whether w occurs in the body of the numeral.

We make use of the following property of the application of two orderedpairs (compare with Barendregt’s hint in his Problem 6.8.15 (ii) [1, Page 149]):

([a_{1}, b_{1}] [a_{2}, b_{2}]) ⟶ ((λx.(x a_{1} b_{1})) (λx.(x a_{2} b_{2})))
⟶ ((λx.(x a_{2} b_{2})) a_{1} b_{1})
⟶ (a_{1} a_{2} b_{2} b_{1})

In particular, we have:

([M, b_{1}] [M, b_{2}]) = (M M b_{2} b_{1})

We define M as follows:

M = λmb_{2}b_{1}.[m, (and b_{1} b_{2})]

By pairing M with F and T we obtain D_{F} and D_{T} respectively:

D_{F} = [M, F]
D_{T} = [M, T]

For any n > 0, the binary expansion of n contains the 1-bit, and so w occurs free in the body of bin_{n}, thus when we substitute D_{F} for w in the body of bin_{n}, the result will be D_{F}. To obtain the test for zero, we only need to take the second projection. We thus define the test for zero as follows:

Zero?_{bin} = λn.(π_{2}^{2} (n D_{T} D_{F}))

Note that as a byproduct of our construction, Zero?_{bin} ignores trailing zeros, so for example:

(Zero?_{bin} (λzw.(z w z z z))) ⟶ F
(Zero?_{bin} (λzw.(z z z z z))) ⟶ T

ii. Let

C = 𝔴𝔡(Zero?_{bin}) + max{𝔴𝔡(π_{2}^{2}([M, b])) : b ∈ {F, T}}
r = max{𝔴𝔡([M, b_{1}] [M, b_{2}]) : b_{1}, b_{2} ∈ {F, T}}

For any n ∈ ℕ, bin_{n} = λzw.b_{1} ⋯ b_{k}, we have:

𝔴𝔡(Zero?_{bin} bin_{n}) ≤ C + 𝔴𝔡(bin_{n}) + k · r
= O(k)
= O(log n)

■

3.2 The Successor Function

3.2.1 Proposition:

i. There exists a combinator Succ?_{bin}, such that for all n ∈ ℕ we have

(Succ?_{bin} bin_{n}) ⟶ bin_{n+1}.

ii. 𝔴𝔡(Succ?_{bin} bin_{n}) = O(log n).

Proof:

i. To compute the successor function on bin_{n}, we need to implement a state machine consisting of three states: The first state, S_{0}, propagates the carry; The second state, S_{1}, goes through the remaining bits after the carry operation has been performed; The third state, S_{2}, is the final state.

The state machine is depicted in the following diagram:

[figure: S_{0}  S_{1}  S_{2}; start; 1; 0; 1; 0; ϵ]

In computing a successor of bin_{n}, we apply bin_{n} to three expressions: The first two substitute for the bits in the body of bin_{n}, and the third expression is used to mark the end of the stream of bits. Each expression needs to have access to

(i) An encoding of the current state (i.e. of either S_{0} or S_{1}), denoted by σ.

(ii) An encoding of whether the given expression is substituted for a 0-bit or a 1-bit, or is a mark for the end of the stream of bits (noted by ϵ in the diagram). This is denoted by b.

(iii) A partial reconstruction of the body of the successive numeral, denoted by r.

The values of (i) and (ii) determine what should the given expression evaluate to. Any finite set of λ-expressions, for which we have a test of equality could therefore be used for encoding (i) and (ii). Furthermore, since the encodings in (i) and (ii) serve only as tags upon which to dispatch, we can eliminate the test altogether by using selectors, i.e. expressions of the form

U_{k}^{n} = λx_{0} ⋯ x_{n}.x_{k}

to encode the various choices. We store this information, and a procedure m in an ordered 4-tuple. Again, observe that:

([m, b_{1}, r_{1}, σ_{1}][m, b_{2}, r_{2}, σ_{2}]) ; \begin{matrix}⟶ ((λx.(x m b_{1} r_{1} σ_{1})) (λx.(x m b_{2} r_{2} σ_{2}))) \\ ⟶ ((λx.(x m b_{2} r_{2} σ_{2})) m b_{1} r_{1} σ_{1}) \\ ⟶ (m m b_{2} r_{2} σ_{2} b_{1} r_{1} σ_{1}) \end{matrix}

As one can see, m is passed a copy of itself, as well as all the information stored in both ordered 4-tuples (both 4-tuples have m is common). On the basis of the information it is passed, m can return the body of the successive numeral or it can construct a new ordered 4-tuple, in which case the computation continues.

Since the particular behaviour of m depends upon many variables, we use Decision-Logic Tables to describe this behaviour in a concise manner.

Decision logic tables (DLT) [7, 8] are a tabular description of how an n-variable function can be used to control selection logic. The format of a DLT is as follows:

list of variable names list of all possible combina-

tions of values of variables

list of actions to be taken selections of combinations of actions as a function of combinations of variables

DLT’s can be formally manipulated and simplified, as well as automatically compiled into computer programs. Since they are not in common use today, we shall avoid the traditional DLT abbreviations, in order to preserve clarity.

The main DLT in our proof distinguishes between the different states. A separate DLT is provided for each state, with the exception of the final state (which does nothing). The three DLT’s are given below:

Main DLT: Determining State

Value of σ_{1}  U_{0}^{1} U_{1}^{1}
Dispatch to the DTL of S_{0} √
Dispatch to the DTL of S_{1}  √

The DLT at S_{0}
Value of b_{1}  U_{0}^{2} U_{0}^{2} U_{0}^{2} U_{1}^{2} U_{1}^{2} U_{1}^{2} U_{2}^{2} U_{2}^{2} U_{2}^{2}
Value of b_{2}  U_{0}^{2} U_{1}^{2} U_{2}^{2} U_{0}^{2} U_{1}^{2} U_{2}^{2} U_{0}^{2} U_{1}^{2} U_{2}^{2}
[m, b_{2}, (r_{1} w), U_{1}^{1}] √ √
(r_{1} w)  √
[m, b_{2}, (r_{1} z), U_{0}^{1}]  √ √
(r_{1} z w)  √
irrelevant  √ √ √

The DLT at S_{1}
Value of b_{1}  U_{0}^{2} U_{0}^{2} U_{0}^{2} U_{1}^{2} U_{1}^{2} U_{1}^{2} U_{2}^{2} U_{2}^{2} U_{2}^{2}
Value of b_{2}  U_{0}^{2} U_{1}^{2} U_{2}^{2} U_{0}^{2} U_{1}^{2} U_{2}^{2} U_{0}^{2} U_{1}^{2} U_{2}^{2}
[m, b_{2}, (r_{1} z), U_{1}^{1}] √ √
(r_{1} z)  √
[m, b_{2}, (r_{1} w), U_{1}^{1}]  √ √
(r_{1} w)  √
irrelevant  √ √ √

As can be seen from the DLT’s for S_{0} and S_{1}, when b_{1} = U_{2}^{2}, the return value is irrelevant. We could return any value whatsoever, so we arbitrarily pick the I combinator. All three DLT’s are combined in M:

M = λmb_{2}r_{2}σ_{2}b_{1}r_{1}σ_{1}.(σ_{1} (b_{1} \begin{matrix}(b_{2} \begin{matrix}[m, b_{2}, (r_{1} w), U_{1}^{1}] \\ [m, b_{2}, (r_{1} w), U_{1}^{1}] \\ (r_{1} w)) \end{matrix} \\ (b_{2} \begin{matrix}[m, b_{2}, (r_{1} z), U_{0}^{1}] \\ [m, b_{2}, (r_{1} z), U_{0}^{1}] \\ (r_{1} z w)) \end{matrix} \\ I) \end{matrix} (b_{1} \begin{matrix}(b_{2} \begin{matrix}[m, b_{2}, (r_{1} z), U_{1}^{1}] \\ [m, b_{2}, (r_{1} z), U_{1}^{1}] \\ (r_{1} z)) \end{matrix} \\ (b_{2} \begin{matrix}[m, b_{2}, (r_{1} w), U_{1}^{1}] \\ [m, b_{2}, (r_{1} w), U_{1}^{1}] \\ (r_{1} w)) \end{matrix} \\ I)) \end{matrix}

We now define the successor function in terms of M as follows:

Succ?_{bin} = λnzw.(n [M, U_{0}^{2}, I, U_{0}^{1}] [M, U_{1}^{2}, I, U_{0}^{1}] [M, U_{2}^{2}, I, U_{0}^{1}])

ii. The proof is similar to the proof of Proposition 3.1.1, albeit more te-

dious. It can be found in our Ph.D. thesis [6]. ■

3.3 The Predecessor Function

3.3.1 Proposition:

i. There exists a combinator Pred?_{bin} such that for all n ∈ ℕ we have

(Pred?_{bin} bin_{n+1}) ⟶ bin_{n}.

ii. 𝔴𝔡(Pred?_{bin} bin_{n}) = O(log n).

Proof:

i. To compute the predecessor function on bin_{n}, we need to implement a state machine consisting of three states: The first state, S_{0}, propagates the carry; The second state, S_{1}, goes through the remaining bits after the carry operation has been performed; The third state, S_{2}, is the final state.

The state machine is depicted in the following diagram:

[figure: S_{0}  S_{1}  S_{2}; start; 0; 1; ϵ; 1; 0; ϵ]

In computing the predecessor of bin_{n}, just as in computing its successor, we apply bin_{n} to three expressions: The first two substitute for the bits in the body of bin_{n}, and the third expression is used to mark the end of the stream of bits. Each expression needs to have access to

(i) An encoding of the current state (i.e. of either S_{0} or S_{1}), denoted by σ.

(ii) An encoding of whether the given expression is substituted for a 0-bit, a 1-bit, or is a mark for the end of the stream of bits. This is denoted by b.

(iii) A partial reconstruction of the body of the preceding numeral, under the assumption that additional z’s in the number are trailing, and should be ignored. This reconstruction is denoted by r_{1}.

(iv) A partial reconstruction of the body of the preceeding numeral, under the assumption that additional z’s in the number are not trailing, and should not be dropped. This reconstruction is denoted by r_{2}.

The values of (i) and (ii) are the same as the corresponding ones in the construction of the successor. Since the predecessor of a bin numeral may have one less bit, we generate two reconstructions of the numeral, in parallel, and commit to one of the two when either a 1-bit or the terminal mark are encountered. Together, (iii) and (iv) correspond to (iii) in the construction of the successor. We store this information, as well as a procedure m, in an ordered 5-tuple. As usual by now, observe that:

([m, b_{1}, r_{11}, r_{12}, σ_{1}] [m, b_{2}, r_{21}, r_{22}, σ_{2}]) ; \begin{matrix}⟶ (\begin{matrix}(λx.(x m b_{1} r_{11} r_{12} σ_{1})) \\ (λx.(x m b_{2} r_{21} r_{22} σ_{2}))) \end{matrix} \\ ⟶ (\begin{matrix}(λx.(x m b_{2} r_{21} r_{22} σ_{2})) \\ m b_{1} r_{11} r_{12} σ_{1}) \end{matrix} \\ ⟶ (m m b_{2} r_{21} r_{22} σ_{2} b_{1} r_{11} r_{12}σ_{1}) \end{matrix}

As one can see, m is passed a copy of itself, and all the information stored in both ordered 5-tuples (again, both ordered 5-tuples have m in common). We use three DLT’s to represent the behaviour of m:

Main DLT: Determining State

Value of σ_{1}  U_{0}^{1} U_{1}^{1}
Dispatch to the DTL of σ_{0} √
Dispatch to the DTL of σ_{1}  √

The DLT at σ_{0}

Value of b_{1}  U_{0}^{2} U_{0}^{2} U_{0}^{2} U_{1}^{2} U_{1}^{2} U_{1}^{2} U_{2}^{2} U_{2}^{2} U_{2}^{2}
Value of b_{2}  U_{0}^{2} U_{1}^{2} U_{2}^{2} U_{0}^{2} U_{1}^{2} U_{2}^{2} U_{0}^{2} U_{1}^{2} U_{2}^{2}
[m, b_{2}, (r_{12} w), (r_{12} w), U_{0}^{1}] √ √
(r_{12} w)  √
[m, b_{2}, r_{11}, (r_{12} z), U_{1}^{1}]  √ √
r_{11}  √
irrelevant  √ √ √

The DLT at σ_{1}
Value of b_{1}  U_{0}^{2} U_{0}^{2} U_{0}^{2} U_{1}^{2} U_{1}^{2} U_{1}^{2} U_{2}^{2} U_{2}^{2} U_{2}^{2}
Value of b_{2}  U_{0}^{2} U_{1}^{2} U_{2}^{2} U_{0}^{2} U_{1}^{2} U_{2}^{2} U_{0}^{2} U_{1}^{2} U_{2}^{2}
[m, b_{2}, r_{11}, (r_{12} z), U_{1}^{1}]  √ √
r_{11}  √
[m, b_{2}, (r_{12} w), (r_{12} w), U_{1}^{1}]  √ √
(r_{12} w)  √
irrelevant  √ √ √

As can be seen from the DLT’s for S_{0} and S_{1}, when b_{1} = U_{2}^{2}, the return value is irrelevant, just like in the derivation of the successor. We could return any value whatsoever, so we once again pick the I combinator. All three DLT’s are combined in M:

M = λmb_{2}r_{21}r_{22}σ_{2}b_{1}r_{11}r_{12}σ_{1}.(σ_{1} (b_{1} \begin{matrix}(b_{2} \begin{matrix}[m, b_{2}, (r_{12} w), (r_{12} w), U_{0}^{1}] \\ [m, b_{2}, (r_{12} w), (r_{12} w), U_{0}^{1}] \\ (r_{12} w)) \end{matrix} \\ (b_{2} \begin{matrix}[m, b_{2}, r_{11}, (r_{12} z), U_{1}^{1}] \\ [m, b_{2}, r_{11}, (r_{12} z), U_{1}^{1}] \\ r_{11}) \end{matrix} \\ I) \end{matrix} (b_{1} \begin{matrix}(b_{2} \begin{matrix}[m, b_{2}, r_{11}, (r_{11} z), U_{1}^{1}] \\ [m, b_{2}, r_{11}, (r_{11} z), U_{1}^{1}] \\ r_{11}) \end{matrix} \\ (b_{2} \begin{matrix}[m, b_{2}, (r_{12} w), (r_{12} w), U_{1}^{1}] \\ [m, b_{2}, (r_{12} w), (r_{12} w), U_{1}^{1}] \\ (r_{12} w)) \end{matrix} \\ I)) \end{matrix}

We now define the predecessor function in terms of M as follows:

Pred?_{bin} = λnzw.(n [M, U_{0}^{2}, z, I, U_{0}^{1}] [M, U_{1}^{2}, z, I, U_{0}^{1}] [M, U_{2}^{2}, z, I, U_{0}^{1}])

Recall that r_{1} contains the partial reconstruction of the preceeding numeral under the assumption that any additional zero bits are trailing, and can therefore be ignored. The initial value of r_{1} must therefore be z, rather than I.

ii. The proof is similar to the proof of Proposition 3.1.1, albeit more tedious. It can be found in our Ph.D. thesis [6].

■

3.4 Adequacy

3.4.1 Proposition: The numeral system bin is adequate.

Proof: Having defined Zero?_{bin}, Succ?_{bin}, and Pred?_{bin}, it follows from Proposition 6.4.3 in Barendregt’s book [1] that bin is an adequate numeral system. ■

4 Conclusion and Assessment

This paper introduces the sequence bin, and shows that it is an adequate numeral system. This section analyses several aspects of bin.

4.1 Extensibility

The definition of bin is easily extensible to other basis, though base 10 might well be the only other useful choice. Similarly, bin can be extended to have a sign, a decimal point and an exponent, facilitating fixed-size floating point arithmetic.

There is some interest in possible representations of real numbers on computers, as streams of decimals or integer coefficients of continued fractions. It is possible that the laziness inherent in the normal order of evaluation could facilitate a lazy numeral system for real numbers as an extension of bin. Such a numeral system would require that certain operations, such as the test for equality and an encoding mechanism (see Section 4.3) be restricted, in order to avoid non-termination. Lazy numbers offer a potential for efficiency, while maintaining the flexibility of carrying on a computation to arbitrary precision.

4.2 Efficiency

Numerals in bin are represented as concisely as possible. The numbertheoretic functions can be computed on bin with the same complexity as they are computed on the standard binary representation used on modern computers. This complexity is independent of the order of evaluation. The use of selectors rather than arbitrary tokens in the dispatching mechanism results in considerable gains in efficiency, and the resulting λ-expressions are both more concise and simpler to verify.

4.3 Implementation

The numeral system bin is extremely suitable for implementation in functional programming languages which model the pure, untyped λ-calculus. We have implemented both the numeral system bin, and the basic numbertheoretic functions defined on it in the Scheme programming language [4]. Our implementation can be combined with the Gödeliser developed as a part of our Ph.D. thesis [5, 6], so that such numerals, as well as possible extensions to the bin numeral system, can be displayed.

4.4 Decision-Logic Tables

Although DLT’s are elaborate and verbose, they are relatively straightforward to construct, and help insure correctness. DLT’s have traditionally been compiled into various programming languages, and so it seems reasonable to expect that λ-expressions for computing more elaborate functions could be generated automatically from a given set of DLT’s.

Acknowledgements

I am grateful to BRICS^{2} for hosting me this summer and for providing a stimulating environment. Thanks are also due to Olivier Danvy, Daniel P. Friedman, and Larry Moss for their comments and encouragement.

The diagrams were drawn with Kristoffer Rose’s XY-pic package.

2

Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

References

[1] Hendrik P. Barendregt. The Lambda Calculus, Its Syntax and Semantics. North-Holland, 1984.

[2] Hendrik P. Barendregt. Personal Communication, Bloomington, Indiana, 1990.

[3] Alonzo Church. The Calculi of Lambda-Conversion. Princeton University Press, 1941.

[4] William Clinger and Jonathan Rees (editors). Revised^{4} report on the algorithmic language Scheme. LISP Pointers, IV(3):1–55, July-September 1991.

[5] Mayer Goldberg. Gödelisation in the λ-calculus. BRICS Research Series RS-95-38, DAIMI, Aarhus University, Denmark, July 1995.

[6] Mayer Goldberg. Recursive Application Survival in the λ-Calculus. PhD thesis, Department of Computer Science, Indiana University, December 1995. Forthcoming.

[7] T.F. Kavanagh. Tabsol – a fundamental concept for system-oriented language. In Proceedings of the Eastern Joint Computer Conference, pages 117–127, New York, December 1960.

[8] Herman McDaniel. An Introduction to Decision Logic Tables. John Wiley & Sons, 1968.

Recent Publications in the BRICS Report Series

RS-95-42 Mayer Goldberg. An Adequate Left-Associated Binary Numeral System in the λ-Calculus. August 1995. 16 pp.

RS-95-41 Olivier Danvy, Karoline Malmkj�r, and Jens Palsberg. Eta-Expansion Does The Trick. August 1995. 23 pp.

RS-95-40 Anna Ing� olfsd� ottir and Andrea Schalk. A Fully Abstract Denotational Model for Observational Congruence. August 1995. 29 pp.

RS-95-39 Allan Cheng. Petri Nets, Traces, and Local Model Checking. July 1995. 32 pp. Full version of paper appearing in Proceedings of AMAST ’95, LNCS 936, 1995.

RS-95-38 Mayer Goldberg. G� odelisation in the λ-Calculus. July 1995. 7 pp.

RS-95-37 Sten Agerholm and Mike Gordon. Experiments with ZF Set Theory in HOL and Isabelle. July 1995. 14 pp. To appear in Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, LNCS, 1995.

RS-95-36 Sten Agerholm. Non-primitive Recursive Function De�nitions. July 1995. 15 pp. To appear in Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, LNCS, 1995.

RS-95-35 Mayer Goldberg. Constructing Fixed-Point Combinators Using Application Survival. June 1995. 14 pp.

RS-95-34 Jens Palsberg. Type Inference with Selftype. June 1995. 22 pp.

RS-95-33 Jens Palsberg, Mitchell Wand, and Patrick O’Keefe. Type Inference with Non-structural Subtyping. June 1995. 22 pp.

RS-95-32 Jens Palsberg. Ef�cient Inference of Object Types. June 1995. 32 pp. To appear in Information and Computation. Preliminary version appears in Ninth Annual IEEE Symposium on Logic in Computer Science, LICS ’94 Proceedings, pages 186�195.