cl-strong: Combinatory Logic Interpreter with Strong (Cβ) Reduction

version 1.0

$Id: cl-strong.html,v 1.8 2009/06/19 21:55:26 bediger Exp $

Bruce Ediger

Table of contents

  1. Introduction
  2. Starting
  3. Using
  4. Cβ Reduction
  5. Building and installing
  6. Bibliography

Introduction

This document describes how to build and use cl-strong v1.0. cl-strong interprets a programming language with a lot of similarities to "Combinatory Logic" (CL) formal systems with basis combinators of S, K,I. It doesn't exactly interpret any "Combinatory Logic" in that it runs on computers with finite CPU speed and a finite memory. Most or all formal systems fail to take these limits into account.

cl-strong performs a variety of reduction known as "Cβ Reduction".

Another page documents the design and implementation of an somewhat different version of a combinatory logic interpreter, one that only does "weak" reduction. That document still holds as a good description of the internals of cl-strong.

Starting the interpreter

After building the interpreter's executable, you can start it from the command line:

 7:57AM 87 % ./cl-strong
STRONG>

The interpreter uses "STRONG>" as its prompt for user input. cl-strong has a strict grammar, so you must type in either a term for reduction, or an interpreter command, or a command to examine an expression.

You have to use keyboard end-of-file (usually control-D) to exit cl-strong.

Giving the interpreter a CL term causes it to execute the usual functional language interpreter's read-eval-print loop. The interpreter prints the input as a minimally-parenthesized expression, Cβ-reduces it to normal form, then prints the normal form. It shows a prompt, then waits for user input.

cl-strong does "Cβ reduction", the scheme described in Boulifa & Mezghiche, Another Implementation Technique for Functional Languages.

Command line options

-ddebug reductions
-eelaborate output
-L filenameLoad and interpret a file named filename
-mon exit, print memory usage summary
-N numberperform up to number reductions
-pDon't print an interactive-use prompt.
-ssingle-step reductions
-T numberevaluate an expression for up to number seconds
-ttrace reductions
-B algorithmUse algorithm as default for bracket abstraction. One of curry or tromp

The -e or -s options have no use without the -t option, but -t alone can perform handy tasks.

-L filename can occur more than one time. cl-strong will interpret the files in order. After the last (or only) file, it prints the STRONG> prompt, then waits for input from the user.

Using the interpreter

Interactive input

I designed cl-strong for use as an interactive system, with a user typing CL expressions at a prompt. The interpreter reduces the expression to a normal form (if it has one), or hits some other limit, like a pre-set timeout, count of allowed reductions or the user's patience.

The interpreter's prompt for input is the string "STRONG>". It appears when the interpreter starts up, or has finished reducing whatever expression the user gave it last, or it has executed an interpreter command.

You have to type an end-of-file character (almost always control-D) to quit, as it has no built-in "exit" or "quit" command.

A keyboard interrupt (almost always control-C) can interrupt whatever long-running reduction currently takes place. The interpreter will display the "STRONG>" prompt after interruption.

A keyboard interrupt at the "STRONG>" prompt will cause the interpreter to exit.

Non-interactive input

The -p command line option causes the interpreter to not print a prompt. This probably only has use for non-interactive input. The interpreter does read from stdin and write to stdout. You can use it as a non-interactive "filter", with input and output redirection.

Grammar, briefly

Grammatically, expressions consist of two terms, and terms consist of either a built-in primitive or a variable or an expression. parentheses can surround expressions.

Built-in primitive have names consisting of a single upper-case letter: S, K and I. Variables (which can also serve as abbreviations) can look like C or Java style identifiers: a letter, followed by zero or more letters or underscores or digits. Non-abbreviation variables act as inert placeholders.

An abstracted variable looks like any identifier surrounded by square brackets. For example, [abc] abstracts a variable named "abc", not 3 variables "a", "b" and "c". The interpreter performs bracket abstraction upon finding an abstracted variable, and uses the resulting expression as a term.

Parentheses

Users can parenthesize input expressions as much or as little as they desire, up to the limits of left-association and the meaning they wish to convey to the interpreter. The grammar used by cl-strong does not allow single variables or primitives inside paired parentheses. It treats terms like "(I)" as syntax errors. You have to put at least 2 primitives and/or variables inside a pair of parentheses, and each parentheses must have a matching counterpart.

The interpreter treats terms as "left associative", the standard in the Combinatory Logic literature. That means that an expression like: I a b c d gets treated as though it had parentheses like this: ((((I a) b) c) d)

To apply one complex term to another, the user must use parentheses. Applying S (S I I) I to S K K would look like this: (S (S I I) I) (S K K).

The interpreter prints out normal formas in minimal-parentheses style. Users can cut-n-paste output into the input, as output has valid input syntax. No keyboard shortcuts exist to re-use any previous input or output.

Built-in Primitives

I built-in 3 primitive combinators. They reduce like this, when given enough arguments:

I a → a
K a b → a
S a b c → a c (b c)

Cβ reduction only has the {S, K, I} basis defined.

Built-in combinators do not necessarily require a certain number (one to three) of arguments to cause a reduction. See the Cβ Reduction section for details.

Bracket Abstraction

"Bracket abstraction" names the process of creating a CL expression without specified variables, that when evaluated with appropriate arguments, ends up giving you the original expression.

The cl-strong interpreter uses the conventional square-bracket notation. For example, to create an expression that will duplicate its single argument, one would type:

STRONG> [x] x x

The x constitutes a "dummy" variable: you can use any valid variable name inside the square brackets. The variable name gets abstracted away, and will not appear in the term that cl-strong calculates.

Bracket abstraction creates an expression, so you can use them where ever you might use any other simple or complex expression, defining an abbreviation, a sub-expression of a much larger expression, as an expression to evaluate immediately, or inside another bracket abstraction. For example, you could create Turing's fixed-point combinator like this:

STRONG> def U [x][y] (x (y y x))
STRONG> def Yturing (U U)

The interpreter uses the expression it calculates for the bracket abstraction of x and y for the definition of the abbreviation U.

Note the use of nested bracket abstractions. The abstraction of y occurs first, then x gets abstracted from the resulting expression.

Algorithms

cl-strong offers 2 different bracket abstraction algorithms. In the following, I use an x to denote any abstracted variable. Abstracted variables can have any syntactically valid variable format.

As near as I can tell, the phrase M, N combinators mean that both terms M and N have no free variables. They contain only built-in primitives.

The curry algorithm is Definition 2.18 in Hindley & Seldin. Hindly & Seldin get very specific about bracket abstraction algorithms in their chapter on "Extensionality in CL". It isn't clear to me that cl-strong works correctly in all circumstances with the tromp algorithm, but I haven't found a specific problem with it. Neither algorithm above matches Boulifa & Mezghiche's bracket abstraction, but again, I can't find any specific problem.

You can set a "default" algorithm with the this command: abstraction name. For name, substitute one of the algorithm names above. cl-strong starts with curry as the default bracket abstraction algorithm.

You can specify an algorithm in the abstraction itself: STRONG> [x]tromp (x (K x))

cl's grammar allows mixing algorithms, one for each variable abstracted. The resulting expression may not make any sense.

Abbreviations

define and def allow a user to introduce "abbreviations" to the input. Each time the abbreviation appears in input, cl-strong makes a copy of the term so abbreviated, and puts it in the input. No matter how complex the expression, an abbreviation still comprises a single term.

def makes an easy-to-type abbreviation of define.

The reduce command actually constitutes an expression, just like a bracket abstraction. Unlike define or def, you can use reduce anywhere an expression would fit, as part of a larger expression, as part of an abbreviation, or as part of a bracket abstraction.

Information about expressions

print lets you see what abbreviations expand to, without evaluation.

The "=" sign lets you determine lexical equality. All combinators, variables and parentheses have to match as strings, otherwise "=" deems the expressions not equivalent. Note that you can include a reduce keyword in either or both of the expressions you compare with "=". Otherwise, it will compare the two expressions without any reduction.

size gives one measure of an expression, the number of atoms, variables, and application nodes in its parse tree. For instance, K (K K) has a size of 5, 3 K atoms, and two applications: (K K) and K applied to (K K).

Intermediate output and single-stepping

You can issue any of these commands without an "on" or "off" argument to inquire about the current state of the directive.

trace, debug and elaborate provide increasingly verbose output. trace shows the expression after each reduction, debug adds information about which branch of an application it evaluates, and elaborate adds to that information useful in debugging memory allocation problems.

step on causes the interpreter to stop after each reduction, print the intermediate expression, and wait, at a ? prompt for user input. Hitting return goes to the next reduction, n or q terminates the reduction, and c (for "continue") causes it to not single-step. cl-strong will carry out any remaining reductions without asking permission.

Reduction information and control

You can turn time outs off by using a 0 (zero) second timeout. Similarly, you can turn reduction-count-limited evaluation off with a 0 (zero) count.

timer on also times bracket abstraction.

Reading files

You only have to double-quote filenames with whitespace in them. You can use absolute filenames (beginning with "/") or you can filenames relative to the current working directory of the cl-strong process.

Cβ Reduction

Cβ Reduction happens according to the following rules.

0.a cβ_m(S)   S
0.b cβ_m(K)   K
0.c cβ_m(I)   I
0.d cβ_m(x)   x for any variable x
1.a cβ_m(SM1M2...Mn)   cβ_m(M1M3(M2M3)M4...Mn) if n ≥ 3
1.b cβ_m(KM1M2...Mn)   cβ_m(M1M3M4...Mn) if n ≥ 2
1.c cβ_m(IM1M2...Mn)   cβ_m(M1M2...Mn) if n ≥ 1
2.a cβ_m(KM1)   λx.cβ_m(M1) where x ∉ FV(M1)
2.b cβ_m(SM1M2)   λx.cβ_m(M1x(M2x) where x ∉ FV(M1, M2)
2.c cβ_m(SM1)   λxy.cβ_m(M1y(xy)) where x,y ∉ FV(M1)
2.d cβ_m(M1M2...Mn)   cβ_m(M1)cβ_m(M2)...cβ_m(Mn) if M1S, K, I
3.a λx.M   [x]β M

No lambda calculus β reductions ever take place. The λs introduced by some Cβ reductions serve only to mark places where a bracket abstraction (via rule 3.a) will take place. Further Combinatory Logic style S, K, I reductions can take place inside the body of a λ abstraction.

According to these rules, an expression in "weak" normal form can reduce further:
S (S (K S) (S (K K) K)) (K (S K K)) K

cl-strong contains one exception to Cβ reduction. Any sub-terms that get duplicated by reduction of an S primitive as in rule (1.a) will appear to get evaluated in parallel. The S primitive in rule (1.a) doesn't copy duplicated terms, it creates links. Any duplicated sub-term gets referenced twice. Reduction of an apparently duplicated sub-term ends up appearing as if all references to that sub-term reduce in parallel. Mezghiche & Boulifa claim that Cβ reduction is confluent, so this "parallel" reduction should not result in non-unique normal forms, should a term have a normal form.

Cβ reduction doesn't seem all that different from Kenneth Loewen's Modified Strong Reduction. except for Cβ rule 2.b vs Loewen's IIb. I don't know what the effect of restricting the second argument of an S to a non-lambda expression might be. I do know that Cβ reduction is specified in a way that makes a computer implementation easy, while Modified Strong Reduction has some ambiguities to resolve.

Example code

Directory tests.in has lots of examples of strong reduction in action, unfortunately mixed in with simpler code that merely exercizes interpreter features, or checks to ensure that a bug doesn't reappear.

Building and installing

  1. Get the source code. You can:
  2. Upack source code. From the command line: tar xzf cl-strong-1.0.tar.gz
  3. Compile source code. From the command line: make gnu.
    That target ("gnu") should work for almost every linux or BSD computer. Other make targets might work better. make cc uses traditionally-unix-named tools, and may work better on Solaris.
  4. At this point, you can test the newly-compiled executable. From the command line: ./runtests. Most of the tests should run quite rapidly, in under a second. At least two of the tests run for 30 seconds or so, and at least one of the tests deliberately provokes a syntax error message from the interpreter.
  5. Install the interpreter if you want, or you can execute it in-place. To install, use the cp or mv commands to move or copy the executable to where ever you want it. It does not care what directory it resides in, and it does not look for configuration files anywhere.

I have built this on x86 Slackware 12.0 Linux, SPARC/Solaris 9 using GCC in both 32- and 64-bit modes, and I've built it on a 64-bit, Opteron-based Red Hat Enterprise Linux 3 system, GCC v3.2.3 I expect it will build easily on any *BSD-based system, but I haven't actually tried that.

I did not have the patience to get it to build on a "PA-RISC" HP-UX system: the ghastly "C89" compiler hated non-ANSI-standard signals, and the "cc" compiler hated function prototypes.

Bibliography

In-print books do not make much mention of strong reduction in Combinatory Logic, the exception being the newly-published Hindley & Seldin book. You mostly have to scrounge for papers on the world wide web.