Format fixes and URL fix in 1998/fanf/README.md
This commit is contained in:
1 parent
c0e237528b
commit
e9196fc245
1 file changed
+100
-65
+100
-65
@@ -6,19 +6,22 @@
|
|||||||
Finchley
|
Finchley
|
||||||
London N3 2QQ
|
London N3 2QQ
|
||||||
United Kingdom
|
United Kingdom
|
||||||
|
<https://dotat.at>
|
||||||
http://www.inch.demon.co.uk/
|
|
||||||
|
|
||||||
## To build:
|
## To build:
|
||||||
|
|
||||||
|
```sh
|
||||||
make all
|
make all
|
||||||
|
```
|
||||||
|
|
||||||
NOTE: This may take a while. Some systems may have problems building
|
NOTE: This may take a while. Some systems may have problems building
|
||||||
this entry because of the system resources it requires.
|
this entry because of the system resources it requires.
|
||||||
|
|
||||||
## To run:
|
## To run:
|
||||||
|
|
||||||
|
```sh
|
||||||
./fanf
|
./fanf
|
||||||
|
```
|
||||||
|
|
||||||
|
|
||||||
### To use:
|
### To use:
|
||||||
@@ -26,6 +29,7 @@ this entry because of the system resources it requires.
|
|||||||
Enter an expression on standard input. Here are some
|
Enter an expression on standard input. Here are some
|
||||||
sample expressions that you can use:
|
sample expressions that you can use:
|
||||||
|
|
||||||
|
```
|
||||||
((\a(\b(\c(d)))) e)
|
((\a(\b(\c(d)))) e)
|
||||||
|
|
||||||
|
|
||||||
@@ -45,6 +49,7 @@ sample expressions that you can use:
|
|||||||
(* n (f (- n 1)))
|
(* n (f (- n 1)))
|
||||||
)
|
)
|
||||||
)
|
)
|
||||||
|
```
|
||||||
|
|
||||||
## Judges' remarks:
|
## Judges' remarks:
|
||||||
|
|
||||||
@@ -55,19 +60,21 @@ impressed by this program!
|
|||||||
See the file [fanf.lambda](fanf.lambda) for more examples of lambda calculus
|
See the file [fanf.lambda](fanf.lambda) for more examples of lambda calculus
|
||||||
source.
|
source.
|
||||||
|
|
||||||
Notice how large the code grows from the fanf.c into the final
|
Notice how large the code grows from the [fanf.c](fanf.c) into the final
|
||||||
fanftmp2.c C program. Take a look at that final C program again,
|
`fanftmp2.c` C program. Take a look at that final C program again,
|
||||||
can you begin to understand what it is doing?
|
can you begin to understand what it is doing?
|
||||||
|
|
||||||
Look at the first stage of the C pre-processing:
|
Look at the first stage of the C pre-processing:
|
||||||
|
|
||||||
|
```sh
|
||||||
cc fanf.c -E > fanftmp1.c
|
cc fanf.c -E > fanftmp1.c
|
||||||
|
```
|
||||||
|
|
||||||
Skip to the bottom of fanftmp1.c (after all of the #include header
|
Skip to the bottom of `fanftmp1.c` (after all of the `#include` header
|
||||||
stuff ... look for a line of the form: # 2 "fanf.c" near the bottom)
|
stuff ... look for a line of the form: `# 2 "fanf.c"` near the bottom)
|
||||||
and look at the resulting code. This code, when C pre-processed
|
and look at the resulting code. This code, when C pre-processed
|
||||||
will expand into over 342 times the original code (ignoring #include
|
will expand into over 342 times the original code (ignoring `#include`
|
||||||
headers) to produce fanftmp2.c. That program in turn, when compiled
|
headers) to produce `fanftmp2.c`. That program in turn, when compiled
|
||||||
translates a single lambda expression on standard input into
|
translates a single lambda expression on standard input into
|
||||||
combinator expressions on standard output.
|
combinator expressions on standard output.
|
||||||
|
|
||||||
@@ -83,8 +90,7 @@ theoretical computer science. The application it implements is a program
|
|||||||
for translating lambda expressions into combinator expressions.
|
for translating lambda expressions into combinator expressions.
|
||||||
|
|
||||||
|
|
||||||
What the program does
|
### What the program does
|
||||||
=====================
|
|
||||||
|
|
||||||
The syntax of lambda expressions recognised by the program is as
|
The syntax of lambda expressions recognised by the program is as
|
||||||
follows: The basic atoms are variables which are single characters other
|
follows: The basic atoms are variables which are single characters other
|
||||||
@@ -102,10 +108,12 @@ simple expression is `(I a)` which is equivalent to `(\x(x) a)`, which
|
|||||||
has the value `a`. Another function called `K` is defined as `\x\y(x)`
|
has the value `a`. Another function called `K` is defined as `\x\y(x)`
|
||||||
and it evaluates as follows:
|
and it evaluates as follows:
|
||||||
|
|
||||||
|
```
|
||||||
K p q
|
K p q
|
||||||
-> \x\y(x) p q
|
-> \x\y(x) p q
|
||||||
-> \y(p) q
|
-> \y(p) q
|
||||||
-> p
|
-> p
|
||||||
|
```
|
||||||
|
|
||||||
Another function of interest is `S`, defined as `\f\g\x((f x) (g x))`.
|
Another function of interest is `S`, defined as `\f\g\x((f x) (g x))`.
|
||||||
My program demonstrates the fact that any lambda expression can be
|
My program demonstrates the fact that any lambda expression can be
|
||||||
@@ -114,6 +122,7 @@ only `S`, `K`, `I` (the combinators), and application, with no
|
|||||||
variables or lambda abstractions. In fact, even `I` is unnecessary,
|
variables or lambda abstractions. In fact, even `I` is unnecessary,
|
||||||
since it is equivalent to `S K K`:
|
since it is equivalent to `S K K`:
|
||||||
|
|
||||||
|
```
|
||||||
I z
|
I z
|
||||||
-> \a(a) z
|
-> \a(a) z
|
||||||
-> z
|
-> z
|
||||||
@@ -123,6 +132,7 @@ since it is equivalent to `S K K`:
|
|||||||
-> (K z) (K z)
|
-> (K z) (K z)
|
||||||
-> \x\y(x) z (K z)
|
-> \x\y(x) z (K z)
|
||||||
-> z
|
-> z
|
||||||
|
```
|
||||||
|
|
||||||
The algorithm for translating lambda expressions into combinator
|
The algorithm for translating lambda expressions into combinator
|
||||||
expressions works as follows. There are three forms of lambda expression
|
expressions works as follows. There are three forms of lambda expression
|
||||||
@@ -143,6 +153,7 @@ abs a `a` -> `I`
|
|||||||
E.g. suppose we had combinator expressions for `+` and `3` and we wanted
|
E.g. suppose we had combinator expressions for `+` and `3` and we wanted
|
||||||
to see what the combinator expression for doubling 3 looked like:
|
to see what the combinator expression for doubling 3 looked like:
|
||||||
|
|
||||||
|
```
|
||||||
trans `\x(+ x x) 3`
|
trans `\x(+ x x) 3`
|
||||||
-> (trans `\x(+ x x)`) (trans `3`)
|
-> (trans `\x(+ x x)`) (trans `3`)
|
||||||
-> (abs x (trans `+ x x`)) `3`
|
-> (abs x (trans `+ x x`)) `3`
|
||||||
@@ -151,99 +162,115 @@ to see what the combinator expression for doubling 3 looked like:
|
|||||||
-> `S` (`S` (abs x `+`) (abs x `x`)) `I` `3`
|
-> `S` (`S` (abs x `+`) (abs x `x`)) `I` `3`
|
||||||
-> `S` (`S` (`K +`) `I`) `I` `3`
|
-> `S` (`S` (`K +`) `I`) `I` `3`
|
||||||
-> `S (S (K +) I) I 3`
|
-> `S (S (K +) I) I 3`
|
||||||
|
```
|
||||||
|
|
||||||
We can then check that this evaluates to the expected result:
|
We can then check that this evaluates to the expected result:
|
||||||
|
|
||||||
|
```
|
||||||
S (S (K +) I) I 3
|
S (S (K +) I) I 3
|
||||||
-> S (K +) I 3 (I 3)
|
-> S (K +) I 3 (I 3)
|
||||||
-> K + 3 (I 3) (I 3)
|
-> K + 3 (I 3) (I 3)
|
||||||
-> + (I 3) (I 3)
|
-> + (I 3) (I 3)
|
||||||
-> + 3 3
|
-> + 3 3
|
||||||
|
```
|
||||||
|
|
||||||
It is possible to perform a slightly more compact translation with a
|
It is possible to perform a slightly more compact translation with a
|
||||||
couple of simple optimisations. For example, note that `K (a b)' is the
|
couple of simple optimisations. For example, note that `K (a b)` is the
|
||||||
same as `S (K a) (K b)', because
|
same as `S (K a) (K b)`, because
|
||||||
|
|
||||||
|
```
|
||||||
K (a b) x
|
K (a b) x
|
||||||
-> a b
|
-> a b
|
||||||
|
```
|
||||||
|
|
||||||
and
|
and
|
||||||
|
|
||||||
|
```
|
||||||
S (K a) (K b) x
|
S (K a) (K b) x
|
||||||
-> K a x (K b x)
|
-> K a x (K b x)
|
||||||
-> a b
|
-> a b
|
||||||
|
```
|
||||||
|
|
||||||
Also, `S (K a) I' is the same as just `a' because
|
Also, `S (K a) I` is the same as just `a` because
|
||||||
|
|
||||||
|
```
|
||||||
S (K a) I x
|
S (K a) I x
|
||||||
-> K a x (I x)
|
-> K a x (I x)
|
||||||
-> a x
|
-> a x
|
||||||
|
```
|
||||||
|
|
||||||
The program simply reads a lambda expression from the standard input,
|
The program simply reads a lambda expression from the standard input,
|
||||||
translates it into a combinator expression using the transformation and
|
translates it into a combinator expression using the transformation and
|
||||||
optimisations described above, and prints out the result.
|
optimisations described above, and prints out the result.
|
||||||
|
|
||||||
|
|
||||||
Why this is a practical application
|
### Why this is a practical application
|
||||||
===================================
|
|
||||||
|
|
||||||
Combinator expressions are easier to evaluate than lambda expressions
|
Combinator expressions are easier to evaluate than lambda expressions
|
||||||
because there are no problems with variables. For example, if I naively
|
because there are no problems with variables. For example, if I naively
|
||||||
evaluated the expression `\x\y(x y) y' I might get `\y(y y)' which is
|
evaluated the expression `\x\y(x y) y` I might get `\y(y y)` which is
|
||||||
not the same as the correct result because the first `y' in the body
|
not the same as the correct result because the first `y` in the body
|
||||||
should refer to a global `y' rather than the local one. David Turner was
|
should refer to a global `y` rather than the local one. David Turner was
|
||||||
the first person to realise that because of this fact, SK combinators
|
the first person to realise that because of this fact, SK combinators
|
||||||
provide a simple way to implement non-strict functional programming
|
provide a simple way to implement non-strict functional programming
|
||||||
languages, either in software or directly in hardware.
|
languages, either in software or directly in hardware.
|
||||||
|
|
||||||
My program demonstrates this by being based on a combinator evaluation
|
My program demonstrates this by being based on a combinator evaluation
|
||||||
engine which is used to implement a language called "OFL" (pronounced
|
engine which is used to implement a language called `OFL` (pronounced
|
||||||
like "offal" and short for "Obfuscated Functional Language"). I then
|
like "offal" and short for "Obfuscated Functional Language"). I then
|
||||||
used OFL to implement all the high-level functionality described above.
|
used `OFL` to implement all the high-level functionality described above.
|
||||||
This contributes a lot to the obfuscation because even small amounts of
|
This contributes a lot to the obfuscation because even small amounts of
|
||||||
OFL are quite unpalatable, and large expressions are completely
|
`OFL` are quite unpalatable, and large expressions are completely
|
||||||
incomprehensible.
|
incomprehensible.
|
||||||
|
|
||||||
It is fairly well known that the lambda calculus (and hence SK
|
It is fairly well known that the lambda calculus (and hence SK
|
||||||
combinators) can compute anything, but mere computation is no use if you
|
combinators) can compute anything, but mere computation is no use if you
|
||||||
cannot communicate with the world. This is why OFL includes a few
|
cannot communicate with the world. This is why `OFL` includes a few
|
||||||
concessions to reality: a combinator `E' for representing characters and
|
concessions to reality: a combinator `E` for representing characters and
|
||||||
testing them for equality, two IO combinators, `G' and `P', for reading
|
testing them for equality, two IO combinators, `G` and `P`, for reading
|
||||||
and writing characters respectively, and a combinator `J' for
|
and writing characters respectively, and a combinator `J` for
|
||||||
representing "false". I also implemented the `Y' combinator directly
|
representing `false`. I also implemented the `Y` combinator directly
|
||||||
rather than in terms of the primitive combinators, since it only
|
rather than in terms of the primitive combinators, since it only
|
||||||
required five characters to do so (viz. `Y W q Q g'). However this code
|
required five characters to do so (viz. `Y W q Q g`). However this code
|
||||||
is not enabled because the definition of Y in terms of other combinators
|
is not enabled because the definition of `Y` in terms of other combinators
|
||||||
is more cute.
|
is more cute.
|
||||||
|
|
||||||
The `E' combinator comes in a large number of forms, one for each
|
The `E` combinator comes in a large number of forms, one for each
|
||||||
character and one for end of file. It is written `E(c)' for the variant
|
character and one for end of file. It is written `E(c)` for the variant
|
||||||
of `E' corresponding to the character `c'. An expression of the form
|
of `E` corresponding to the character `c`. An expression of the form
|
||||||
`E(c) x' is evaluated by first evaluating `x'. If `x' doesn't evaluate
|
`E(c) x` is evaluated by first evaluating `x`. If `x` doesn't evaluate
|
||||||
to some form of `E', then evaluation of the expression terminates. If
|
to some form of `E`, then evaluation of the expression terminates. If
|
||||||
`x' evaluates to `E(c)', then the expression evaluates to `K'. If `x'
|
`x` evaluates to `E(c)`, then the expression evaluates to `K`. If `x`
|
||||||
evaluates to `E(d)' (where `d' is a different character to `c'), then
|
evaluates to `E(d)` (where `d` is a different character to `c`), then
|
||||||
the expression evaluates to `J'.
|
the expression evaluates to `J`.
|
||||||
|
|
||||||
`K' and `J' are used to represent "true" and "false" respectively; they
|
`K` and `J` are used to represent `true` and `false` respectively; they
|
||||||
correspond exactly to the standard lambda calculus representations of
|
correspond exactly to the standard lambda calculus representations of
|
||||||
true and false, viz. `\t\f(t)' and `\t\f(f)' respectively. In this way a
|
true and false, viz. `\t\f(t)` and `\t\f(f)` respectively. In this way a
|
||||||
conditional expression can just be written `cond then else', which is
|
conditional expression can just be written `cond then else`, which is
|
||||||
even more terse than C's `cond ? then : else'. An expression that
|
even more terse than C `cond ? then : else`. An expression that
|
||||||
compares a character with `a', say, can be written in the rather
|
compares a character with `a`, say, can be written in the rather
|
||||||
obfuscated form `E('a') char then else'.
|
obfuscated form `E('a') char then else`.
|
||||||
|
|
||||||
The `P' combinator, like the `E' combinator, starts off by evaluating
|
The `P` combinator, like the `E` combinator, starts off by evaluating
|
||||||
its first argument and checking that it is some form of `E'. It then
|
its first argument and checking that it is some form of `E`. It then
|
||||||
writes that character on stdout, and finally it calls its second
|
writes that character on stdout, and finally it calls its second
|
||||||
argument as a function with the argument `I', i.e.
|
argument as a function with the argument `I`, i.e.
|
||||||
|
|
||||||
|
```
|
||||||
P x f -> f I
|
P x f -> f I
|
||||||
|
```
|
||||||
|
|
||||||
with a side-effect.
|
with a side-effect.
|
||||||
|
|
||||||
The `G' combinator just reads a character from stdin then calls its
|
The `G` combinator just reads a character from stdin then calls its
|
||||||
argument as a function with the appropriate `E' combinator as an
|
argument as a function with the appropriate `E` combinator as an
|
||||||
argument, i.e.
|
argument, i.e.
|
||||||
|
|
||||||
|
```
|
||||||
G f -> f E(c)
|
G f -> f E(c)
|
||||||
|
```
|
||||||
|
|
||||||
with a side-effect.
|
with a side-effect.
|
||||||
|
|
||||||
One of the problems with non-strict languages is that it is hard to
|
One of the problems with non-strict languages is that it is hard to
|
||||||
@@ -256,41 +283,51 @@ We can then check that this evaluates to the expected result:
|
|||||||
CPS form of the IO monad from page 6 of "Imperative Functional
|
CPS form of the IO monad from page 6 of "Imperative Functional
|
||||||
Programming".)
|
Programming".)
|
||||||
|
|
||||||
The `Y' combinator is used for implementing recursive functions. It has
|
The `Y` combinator is used for implementing recursive functions. It has
|
||||||
the evaluation rule
|
the evaluation rule
|
||||||
|
|
||||||
|
```
|
||||||
Y f -> f (Y f)
|
Y f -> f (Y f)
|
||||||
|
```
|
||||||
|
|
||||||
so that it can be used to call a function with itself as an argument.
|
so that it can be used to call a function with itself as an argument.
|
||||||
For example, if I had the appropriate arithmetic operators defined, I
|
For example, if I had the appropriate arithmetic operators defined, I
|
||||||
could write a factorial function in the lambda calculus like this:
|
could write a factorial function in the lambda calculus like this:
|
||||||
Y \f\n((= n 0) 1 (* n (f (- n 1))))
|
|
||||||
|
|
||||||
OFL provides a facility for naming expressions so that they can be used
|
```
|
||||||
|
Y \f\n((= n 0) 1 (* n (f (- n 1))))
|
||||||
|
```
|
||||||
|
|
||||||
|
`OFL` provides a facility for naming expressions so that they can be used
|
||||||
more than once without writing them in full. A definition must be written
|
more than once without writing them in full. A definition must be written
|
||||||
on one line in the form `l name b expression' where `l' is short for
|
on one line in the form `l name b expression` where `l` is short for
|
||||||
"let" and `b' is short for "be". Names must be more than one character
|
"let" and `b` is short for "be". Names must be more than one character
|
||||||
long. A complete OFL program starts off by defining the primitives it
|
long. A complete `OFL` program starts off by defining the primitives it
|
||||||
will use with likes of the form `p (S)' etc., then goes on to define the
|
will use with likes of the form `p (S)` etc., then goes on to define the
|
||||||
names it will use, and finishes off with the main expression followed by
|
names it will use, and finishes off with the main expression followed by
|
||||||
a single `e' short for "end". OFL expressions must use the minimum
|
a single `e` short for "end". `OFL` expressions must use the minimum
|
||||||
number of brackets needed to be unambiguous, except that the whole
|
number of brackets needed to be unambiguous, except that the whole
|
||||||
expression must be surrounded by brackets.
|
expression must be surrounded by brackets.
|
||||||
|
|
||||||
OFL has a standard library which adds another five combinators to the
|
`OFL` has a standard library which adds another five combinators to the
|
||||||
basic eight. These combinators provide greater scope for optimisation
|
basic eight. These combinators provide greater scope for optimisation
|
||||||
when translating an expression from the lambda calculus to combinators,
|
when translating an expression from the lambda calculus to combinators,
|
||||||
and therefore more compact programs. Their evaluation rules are:
|
and therefore more compact programs. Their evaluation rules are:
|
||||||
|
|
||||||
|
```
|
||||||
B f g x -> f (g x)
|
B f g x -> f (g x)
|
||||||
C f g x -> (f x) g
|
C f g x -> (f x) g
|
||||||
BB c f g x -> c (f (g x))
|
BB c f g x -> c (f (g x))
|
||||||
CC c f g x -> c (f x) g
|
CC c f g x -> c (f x) g
|
||||||
SS c f g x -> c (f x) (g x)
|
SS c f g x -> c (f x) (g x)
|
||||||
|
```
|
||||||
|
|
||||||
I used them to help fit my program into the required space; unfortunately
|
I used them to help fit my program into the required space; unfortunately
|
||||||
I couldn't fit the version that fully optimises the lambda expressions
|
I couldn't fit the version that fully optimises the lambda expressions
|
||||||
it reads into the required space. The complete optimisation rules
|
it reads into the required space. The complete optimisation rules
|
||||||
including the ones it doesn't use are:
|
including the ones it doesn't use are:
|
||||||
|
|
||||||
|
```
|
||||||
S (K p) I -> p
|
S (K p) I -> p
|
||||||
S (K p) (K r) -> K ( p r )
|
S (K p) (K r) -> K ( p r )
|
||||||
S (K p) (B r s) -> BB p r s
|
S (K p) (B r s) -> BB p r s
|
||||||
@@ -299,13 +336,12 @@ We can then check that this evaluates to the expected result:
|
|||||||
S p (K r) -> C p r
|
S p (K r) -> C p r
|
||||||
S (B p q) r -> SS p q r
|
S (B p q) r -> SS p q r
|
||||||
S p r -> S p r
|
S p r -> S p r
|
||||||
|
```
|
||||||
|
|
||||||
|
### The implementation of `OFL`
|
||||||
|
|
||||||
The implementation of OFL
|
Although `OFL` has completely different syntax and semantics to C, all you
|
||||||
=========================
|
need to compile `OFL` programs is a C compiler and a header file (which in
|
||||||
|
|
||||||
Although OFL has completely different syntax and semantics to C, all you
|
|
||||||
need to compile OFL programs is a C compiler and a header file (which in
|
|
||||||
my entry to the competition has been included in-line). The header file
|
my entry to the competition has been included in-line). The header file
|
||||||
implements a two-pass optimising compiler which produces a representation
|
implements a two-pass optimising compiler which produces a representation
|
||||||
of the program that is then interpreted.
|
of the program that is then interpreted.
|
||||||
@@ -327,8 +363,8 @@ We can then check that this evaluates to the expected result:
|
|||||||
rules of the combinators that I described above.
|
rules of the combinators that I described above.
|
||||||
|
|
||||||
The first 54 lines of the program are mostly the interpreter; the next 8
|
The first 54 lines of the program are mostly the interpreter; the next 8
|
||||||
lines are pass one of the compiler; the next nine declare the OFL
|
lines are pass one of the compiler; the next nine declare the `OFL`
|
||||||
primitives; the next five define the OFL standard library; and the rest
|
primitives; the next five define the `OFL` standard library; and the rest
|
||||||
implement the application described in the first part of this document.
|
implement the application described in the first part of this document.
|
||||||
This part of the program is transformed into the second pass of the
|
This part of the program is transformed into the second pass of the
|
||||||
compiler by the first pass of the compiler.
|
compiler by the first pass of the compiler.
|
||||||
@@ -350,8 +386,7 @@ We can then check that this evaluates to the expected result:
|
|||||||
implements the tail recursion optimisation, which is probably not true.
|
implements the tail recursion optimisation, which is probably not true.
|
||||||
|
|
||||||
|
|
||||||
References
|
### References
|
||||||
==========
|
|
||||||
|
|
||||||
I used these references in the course of writing this program and they
|
I used these references in the course of writing this program and they
|
||||||
explain some of the ideas behind it in more detail. Arthur Norman (one
|
explain some of the ideas behind it in more detail. Arthur Norman (one
|
||||||
|
|||||||
Reference in new issue
Block a user