Move 1988-2004 entries into subdirs
We we move 1988-2004 entries from all of a year's winning entries in a single directory to each winner being in their own sub-directory under the given year directory.
This commit is contained in:
Landon Curt Noll committed
1 parent
1e82e8aa3e
commit
d2a42f42e8
478 files changed
No files matched your search
@@ -0,0 +1,120 @@
|
||||
#include <stdlib.h>
|
||||
#include <stdio.h>
|
||||
#define l #define
|
||||
#define p(p) l p b ( m p u X )
|
||||
|
||||
l i int
|
||||
l n struct n
|
||||
l x ){ return (
|
||||
l A ->
|
||||
l N n*
|
||||
|
||||
n { i c ; N L ; N R ; N U ; N ( * F ) ( N ) ; } ;
|
||||
|
||||
l F A F
|
||||
l U A U
|
||||
l R A R
|
||||
l L A L
|
||||
l m q = malloc(sizeof * q ) Z F =
|
||||
l e z F ( p ) ) ; }
|
||||
l f e N
|
||||
l g z L Q s f
|
||||
l h ( N p x
|
||||
l H h p L U Q
|
||||
l s R z R = q
|
||||
l t ) ? p : (
|
||||
l z , p
|
||||
l Z , q
|
||||
l Q = p
|
||||
l w ! p U t p U L Q z Q U ,
|
||||
l D W p R U = 0 z R Q R F ( p R ) z R F != E t
|
||||
l W h w
|
||||
l X z = q , 0
|
||||
l V w p F = v z L Q
|
||||
l O m o Z L Q
|
||||
l M m E Z A c =
|
||||
l r Z R Q
|
||||
l u Z U Q
|
||||
l a ) ) ) ? 0 : j ( !
|
||||
l k ( i c x
|
||||
l y 0 ) ; } i
|
||||
|
||||
N q ; N
|
||||
o H z Q L f
|
||||
v H U z Q L f
|
||||
K W V L R f
|
||||
J W V R f
|
||||
I h V R f
|
||||
#if 0
|
||||
Y W q Q g
|
||||
#endif
|
||||
S W w w O L L R r s , O L R r R R g
|
||||
E D p F Q L A c - p R A c ? J : K f
|
||||
P D w putchar ( p L R A c ) , m I g
|
||||
G W M getchar ( ) g
|
||||
p ;
|
||||
|
||||
i j k c ? O U r u U U X : y b k y d k y
|
||||
|
||||
l d(d) ( ( d a b
|
||||
l b(b) ( ( b a d
|
||||
l E(E) b ( M E u X )
|
||||
|
||||
main k i ) ! (
|
||||
|
||||
p (I)
|
||||
p (J)
|
||||
p (K)
|
||||
#if 0
|
||||
p (Y)
|
||||
#endif
|
||||
p (P)
|
||||
p (G)
|
||||
|
||||
p (S)
|
||||
l B b (S (K S) K)
|
||||
l SS b (B (B S) B)
|
||||
l C b (SS B S (K K))
|
||||
l CC b (B (B C) B)
|
||||
l BB b (CC B (B B B) B)
|
||||
|
||||
l Y b (S (C B (S I I)) (C B (S I I)))
|
||||
|
||||
l CI b (C I)
|
||||
|
||||
l ef E(EOF)
|
||||
l sp E(' ')
|
||||
l ob E('(')
|
||||
l cb E(')')
|
||||
l lm E('\\')
|
||||
l nl E('\n')
|
||||
l ht E('\t')
|
||||
l qs E('S')
|
||||
l qk E('K')
|
||||
l qi E('I')
|
||||
|
||||
l pair b (BB (B (B K)) C CI)
|
||||
l atom b (B K CI)
|
||||
|
||||
l bind b (CC B B C)
|
||||
|
||||
l ore b (SS (CI K))
|
||||
l gns b (Y (B (bind G) (CC S (C (ore sp (ore nl ht))) CI)))
|
||||
|
||||
l pr b (Y (CC C (BB CI (B (BB (bind (P ob)) K)) (SS C (CC C (BB BB bind) K) (C (CC bind) (K (P cb))))) P))
|
||||
|
||||
l trans b (Y (B (bind gns) (S (BB S (C lm) lam) (C (BB S (C ob) brac) (S (C cb (CI (atom sp))) (S (C ef (CI (atom sp))) (B CI atom)))))))
|
||||
|
||||
l brac b (S bind (B Y (C (BB B B bind) (S (BB S (BB S (S I)) (CC (BB (B K)) (BB K) pair)) (CC S (CC BB (BB C (C (CI sp)) CI)) pair)))))
|
||||
|
||||
l lam b (B (bind gns) (C (CC BB bind (B CI)) abs))
|
||||
|
||||
l abs b (Y (C (BB S (BB C CI) (SS S (BB C (BB B opt)) I)) (CC S (C C (atom qi)) (B (pair (atom qk)) atom))))
|
||||
|
||||
l make b (B pair (pair (atom qs)))
|
||||
|
||||
l opt b (S (S I (S (BB (CC B) CI (BB K K make)) (S (BB C (BB C (C (CI qk))) (SS (SS S) (S (BB (BB (S I)) S (BB (BB (CC B) CI) (BB K K) make)) (B (CC B (BB (CC C) (BB (C (CI qk)) (pair (atom qk))) pair)) make)) (B (C (BB B C (C (CI qi)))) make))) make))) (B K make))
|
||||
|
||||
(bind (bind trans pr) (P nl) I)
|
||||
|
||||
e
|
||||
@@ -0,0 +1,388 @@
|
||||
Most Obfuscated Translator:
|
||||
|
||||
Tony Finch
|
||||
Demon Internet
|
||||
322 Regent's Park Road
|
||||
Finchley
|
||||
London N3 2QQ
|
||||
United Kingdom
|
||||
|
||||
http://www.inch.demon.co.uk/
|
||||
|
||||
|
||||
Judges' comments:
|
||||
|
||||
To build:
|
||||
make fanf
|
||||
|
||||
Some systems may have problems building this entry because
|
||||
of the system resources can require.
|
||||
|
||||
To use:
|
||||
Enter an expression on standard input. Here are some
|
||||
sample expressions that you can use:
|
||||
|
||||
((\a(\b(\c(d)))) e)
|
||||
|
||||
|
||||
(\f\g\x
|
||||
(
|
||||
(g x) (f x)
|
||||
) K K z
|
||||
)
|
||||
|
||||
|
||||
(\f(\f\g\x( (f((\a(g(b))) e)) (g x) ) K K z))
|
||||
|
||||
|
||||
(Y\f\n
|
||||
((= n 0)
|
||||
1
|
||||
(* n (f (- n 1)))
|
||||
)
|
||||
)
|
||||
|
||||
This program translares lambda expressions into combinator
|
||||
expressions. But you do not need to know Lambda Calculus to be
|
||||
impressed by this program!
|
||||
|
||||
See the file:
|
||||
|
||||
fanf.lambda
|
||||
|
||||
for more examples of lambda calculus source.
|
||||
|
||||
Notice how large the code grows from the fanf.c into the final
|
||||
fanftmp2.c C program. Take a look at that final C program again,
|
||||
can you begin to understand what it is doing?
|
||||
|
||||
Look at the first stage of the C pre-processing:
|
||||
|
||||
gcc -ansi fanf.c -E > fanftmp1.c
|
||||
|
||||
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)
|
||||
and look at the resulting code. This code, when C pre-processed
|
||||
will expand into over 342 times the original code (ignoring #include
|
||||
headers) to produce fanftmp2.c. That program in turn, when compiled
|
||||
translates a single lambda expression on standard input into
|
||||
combinator expressions on standard output.
|
||||
|
||||
Extra credit question:
|
||||
|
||||
What do you have to do to make this program work with an
|
||||
old non-ANSI C preprocessor?
|
||||
|
||||
|
||||
Selected Author's comments:
|
||||
|
||||
My program is a demonstration of some practical applications of
|
||||
theoretical computer science. The application it implements is a program
|
||||
for translating lambda expressions into combinator expressions.
|
||||
|
||||
|
||||
What the program does
|
||||
=====================
|
||||
|
||||
The syntax of lambda expressions recognised by the program is as
|
||||
follows: The basic atoms are variables which are single characters other
|
||||
than backslash or parentheses, e.g. `a' or `b' or `@'. Variables are
|
||||
combined by function application which is written e.g. `(f a)' which is
|
||||
the function `f' applied to the argument `a'. Application groups to the
|
||||
left, so `(f a b c)' is equivalent to `(((f a) b) c)'. Functions are
|
||||
created from lambda terms which are written in the form `\a(expr)' which
|
||||
is the function taking argument `a' and having value `expr'. Lambda is
|
||||
spelt `\' because ASCII isn't good enough. Lambda binds tightly, so
|
||||
`\a\bcd' is equivalent to `((\a(\b(c))) d)'. Whitespace is ignored.
|
||||
|
||||
For example, the identity function, called `I', is written `\x(x)'. A
|
||||
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)'
|
||||
and it evaluates as follows:
|
||||
|
||||
K p q
|
||||
-> \x\y(x) p q
|
||||
-> \y(p) q
|
||||
-> p
|
||||
|
||||
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
|
||||
translated into an equivalent "combinator expression" which involves
|
||||
only `S', `K', `I' (the combinators), and application, with no
|
||||
variables or lambda abstractions. In fact, even `I' is unnecessary,
|
||||
since it is equivalent to `S K K':
|
||||
|
||||
I z
|
||||
-> \a(a) z
|
||||
-> z
|
||||
|
||||
S K K z
|
||||
-> \f\g\x((f x) (g x)) K K z
|
||||
-> (K z) (K z)
|
||||
-> \x\y(x) z (K z)
|
||||
-> z
|
||||
|
||||
The algorithm for translating lambda expressions into combinator
|
||||
expressions works as follows. There are three forms of lambda expression
|
||||
to consider: variables, applications, and abstractions.
|
||||
|
||||
trans `v' -> `v' (variable)
|
||||
trans `a b' -> (trans `a') (trans `b') (application)
|
||||
trans `\ab' -> abs a (trans `b') (abstraction)
|
||||
|
||||
There are a further three cases to consider for the body of lambda
|
||||
expressions, where we need to do the magic that transforms away the
|
||||
variables.
|
||||
|
||||
abs a `f x' -> `S' (abs a `f') (abs a `x')
|
||||
abs a `b' -> `K b' (b != a)
|
||||
abs a `a' -> `I'
|
||||
|
||||
E.g. suppose we had combinator expressions for `+' and `3' and we wanted
|
||||
to see what the combinator expression for doubling 3 looked like:
|
||||
|
||||
trans `\x(+ x x) 3'
|
||||
-> (trans `\x(+ x x)') (trans `3')
|
||||
-> (abs x (trans `+ x x')) `3'
|
||||
-> (abs x `+ x x') `3'
|
||||
-> `S' (abs x `+ x') (abs x `x') `3'
|
||||
-> `S' (`S' (abs x `+') (abs x `x')) `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:
|
||||
|
||||
S (S (K +) I) I 3
|
||||
-> S (K +) I 3 (I 3)
|
||||
-> K + 3 (I 3) (I 3)
|
||||
-> + (I 3) (I 3)
|
||||
-> + 3 3
|
||||
|
||||
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
|
||||
same as `S (K a) (K b)', because
|
||||
|
||||
K (a b) x
|
||||
-> a b
|
||||
|
||||
and
|
||||
|
||||
S (K a) (K b) x
|
||||
-> K a x (K b x)
|
||||
-> a b
|
||||
|
||||
Also, `S (K a) I' is the same as just `a' because
|
||||
|
||||
S (K a) I x
|
||||
-> K a x (I x)
|
||||
-> a x
|
||||
|
||||
The program simply reads a lambda expression from the standard input,
|
||||
translates it into a combinator expression using the transformation and
|
||||
optimisations described above, and prints out the result.
|
||||
|
||||
|
||||
Why this is a practical application
|
||||
===================================
|
||||
|
||||
Combinator expressions are easier to evaluate than lambda expressions
|
||||
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
|
||||
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
|
||||
the first person to realise that because of this fact, SK combinators
|
||||
provide a simple way to implement non-strict functional programming
|
||||
languages, either in software or directly in hardware.
|
||||
|
||||
My program demonstrates this by being based on a combinator evaluation
|
||||
engine which is used to implement a language called "OFL" (pronounced
|
||||
like "offal" and short for "Obfuscated Functional Language"). I then
|
||||
used OFL to implement all the high-level functionality described above.
|
||||
This contributes a lot to the obfuscation because even small amounts of
|
||||
OFL are quite unpalatable, and large expressions are completely
|
||||
incomprehensible.
|
||||
|
||||
It is fairly well known that the lambda calculus (and hence SK
|
||||
combinators) can compute anything, but mere computation is no use if you
|
||||
cannot communicate with the world. This is why OFL includes a few
|
||||
concessions to reality: a combinator `E' for representing characters and
|
||||
testing them for equality, two IO combinators, `G' and `P', for reading
|
||||
and writing characters respectively, and a combinator `J' for
|
||||
representing "false". I also implemented the `Y' combinator directly
|
||||
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
|
||||
is not enabled because the definition of Y in terms of other combinators
|
||||
is more cute.
|
||||
|
||||
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
|
||||
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
|
||||
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'
|
||||
evaluates to `E(d)' (where `d' is a different character to `c'), then
|
||||
the expression evaluates to `J'.
|
||||
|
||||
`K' and `J' are used to represent "true" and "false" respectively; they
|
||||
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
|
||||
conditional expression can just be written `cond then else', which is
|
||||
even more terse than C's `cond ? then : else'. An expression that
|
||||
compares a character with `a', say, can be written in the rather
|
||||
obfuscated form `E('a') char then else'.
|
||||
|
||||
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
|
||||
writes that character on stdout, and finally it calls its second
|
||||
argument as a function with the argument `I', i.e.
|
||||
P x f -> f I
|
||||
with a side-effect.
|
||||
|
||||
The `G' combinator just reads a character from stdin then calls its
|
||||
argument as a function with the appropriate `E' combinator as an
|
||||
argument, i.e.
|
||||
G f -> f E(c)
|
||||
with a side-effect.
|
||||
|
||||
One of the problems with non-strict languages is that it is hard to
|
||||
predict in advance in which order side-effects will occur. In my program
|
||||
I used a monadic IO structure like that used by the programming language
|
||||
Haskell; this allows one to write programs that manipulate external
|
||||
state in a manner remarkably similar to imperative programming languages
|
||||
like C. An examination of my program should provide an illustration of
|
||||
how well this technique works in practice. (In particular, I used the
|
||||
CPS form of the IO monad from page 6 of "Imperative Functional
|
||||
Programming".)
|
||||
|
||||
The `Y' combinator is used for implementing recursive functions. It has
|
||||
the evaluation rule
|
||||
Y f -> f (Y f)
|
||||
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
|
||||
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
|
||||
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
|
||||
"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
|
||||
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
|
||||
a single `e' short for "end". OFL expressions must use the minimum
|
||||
number of brackets needed to be unambiguous, except that the whole
|
||||
expression must be surrounded by brackets.
|
||||
|
||||
OFL has a standard library which adds another five combinators to the
|
||||
basic eight. These combinators provide greater scope for optimisation
|
||||
when translating an expression from the lambda calculus to combinators,
|
||||
and therefore more compact programs. Their evaluation rules are:
|
||||
|
||||
B f g x -> f (g x)
|
||||
C f g x -> (f x) g
|
||||
BB c f g x -> c (f (g x))
|
||||
CC c f g x -> c (f x) g
|
||||
SS c f g x -> c (f x) (g x)
|
||||
|
||||
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
|
||||
it reads into the required space. The complete optimisation rules
|
||||
including the ones it doesn't use are:
|
||||
|
||||
S (K p) I -> p
|
||||
S (K p) (K r) -> K ( p r )
|
||||
S (K p) (B r s) -> BB p r s
|
||||
S (K p) r -> B p r
|
||||
S (B p q) (K r) -> CC p q r
|
||||
S p (K r) -> C p r
|
||||
S (B p q) r -> SS p q r
|
||||
S p r -> S p r
|
||||
|
||||
|
||||
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
|
||||
my entry to the competition has been included in-line). The header file
|
||||
implements a two-pass optimising compiler which produces a representation
|
||||
of the program that is then interpreted.
|
||||
|
||||
The first pass of the compiler is implemented via the C preprocessor. It
|
||||
implements one optimisation, namely function in-lining. Unfortunately,
|
||||
this optimisation always increases object code size and execution time.
|
||||
The opposite optimisation, common sub-expression elimination, (which
|
||||
would offer improvements in code size and execution time) has not been
|
||||
implemented. The output of this pass is a C program that may be compiled
|
||||
by a normal C compiler.
|
||||
|
||||
The second pass is performed by the initialisation phase of the C
|
||||
program. It builds a data structure representing the abstract syntax
|
||||
tree of the program.
|
||||
|
||||
The program is then executed by an interpreter. This operates by
|
||||
performing manipulations on the AST that correspond to the evaluation
|
||||
rules of the combinators that I described above.
|
||||
|
||||
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
|
||||
primitives; the next five define the OFL standard library; and the rest
|
||||
implement the application described in the first part of this document.
|
||||
This part of the program is transformed into the second pass of the
|
||||
compiler by the first pass of the compiler.
|
||||
|
||||
The first pass of the compiler relies on some magic macros that expand
|
||||
in a mutually-overlapping and almost recursive way in order to
|
||||
perpetrate a complete change of syntax. Interestingly enough, if I
|
||||
hadn't used the same identifier for more than one thing in various
|
||||
places in the program this transformation would work with old-style cpp
|
||||
as well and ANSI cpp. It expands the program from about 2.2KB to about
|
||||
740KB. The resulting code does some tricky stuff to build a data
|
||||
structure of the same form as the code itself.
|
||||
|
||||
The interpreter is written in fairly straightforward C, although it is
|
||||
highly compressed. The C itself is written in a fairly functional style,
|
||||
in that every function consists of a single expression. In the tradition
|
||||
of functional programming languages it assumes that memory is infinite
|
||||
and so never frees anything. It also assumes that the C compiler
|
||||
implements the tail recursion optimisation, which is probably not true.
|
||||
|
||||
|
||||
References
|
||||
==========
|
||||
|
||||
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
|
||||
of the authors of the first paper) did a lot to enthuse me about this
|
||||
topic.
|
||||
|
||||
Clarke, T. J. W., et al., 1980. SKIM - the S, K, I Reduction Machine.
|
||||
Proceedings of the 1980 ACM LISP Conference, pp. 128-135.
|
||||
|
||||
Curry, H. B. and Feys, R., 1958. Combinatory Logic, Vol. 1.
|
||||
North-Holland.
|
||||
|
||||
Gordon, M. J. C., 1988. Programming Language Theory and its
|
||||
Implementation. Prentice-Hall.
|
||||
|
||||
Peterson, J, et al., 1997. Report on the Programming Language Haskell,
|
||||
version 1.4.
|
||||
|
||||
Peyton Jones, S. L., 1987. The implementation of Functional
|
||||
Programming Languages, Chapters 2, 11, 12, 16. Prentice-Hall.
|
||||
|
||||
Peyton Jones, S. L., and Wadler, P., 1992. Imperative Functional
|
||||
Programming. Proceedings of the ACM Symposium on the Principles of
|
||||
Programming Languages 1993, pp. 71-84.
|
||||
|
||||
Turner, D. A., 1979. A new implementation technique for applicative
|
||||
languages. Software- Practice and Experience. Vol. 9, pp. 31-49.
|
||||
|
||||
Turner, D. A., 1979. Another algorithm for bracket abstraction. Journal
|
||||
of Symbolic Logic. Vol. 44, no. 2, pp. 67-270.
|
||||
|
||||
Wadler, P., 1990. Comprehending Monads. Proceedings of the ACM
|
||||
conference on Lisp and Functional Programming, 1990.
|
||||
|
||||
Wadler, P., 1995. How to Declare an Imperative. Proceedings of the ACM
|
||||
International Logic Programming Symposium, 1995.
|
||||
@@ -0,0 +1,262 @@
|
||||
-----------------------------------------------------------------------------
|
||||
--
|
||||
-- This file contains the original source code for my entry, which was
|
||||
-- written in the lambda calculus using a slightly extended syntax
|
||||
-- compared to that accepted by my entry (in particular, it has
|
||||
-- multi-character identifiers and uses ` instead of \ because that's
|
||||
-- easier to enter inside a Haskell string). It also contains the Haskell
|
||||
-- code I used to translate the lambda calculus into combinators using
|
||||
-- the fully optimising algorithm described in the .hint file.
|
||||
--
|
||||
-- Tony Finch <dot@dotat.at>
|
||||
--
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
--
|
||||
-- Source code for my entry
|
||||
--
|
||||
|
||||
|
||||
unit = `val`k(k val)
|
||||
= CI
|
||||
bind = `op`fop`k(op `res(fop res k))
|
||||
= (CC B B C)
|
||||
|
||||
|
||||
revacc = Y `f(`acc`list(list `nil(acc)
|
||||
`head`tail(f tail (pair head acc))))
|
||||
rev = revacc I
|
||||
|
||||
fold = `atomf`pairf(Y `rec(`list(list atomf (pairf rec))))
|
||||
= (B (B Y) (BB B C CI))
|
||||
|
||||
|
||||
pair = `x`y`f`g( f x y )
|
||||
atom = `a`f`g( g a )
|
||||
|
||||
|
||||
ore = `a`b`c(a c K (b c)) = (SS (CI K))
|
||||
gns = Y `f(bind G `c(ore sp (ore nl ht) c f (C I c)))
|
||||
|
||||
pr = Y `f`e(e `x`y(bind (P ob) `i(bind (f x) `i(bind (f y) `i(P cb))))
|
||||
`a(P a))
|
||||
|
||||
trans = Y `f(bind gns `c( lm c (lambda f)
|
||||
ob c (brac f)
|
||||
cb c (unit (atom sp))
|
||||
ef c (unit (atom sp))
|
||||
(unit (atom c)) ))
|
||||
|
||||
brac = `f(bind f (Y `l`ea(bind f `eb(eb `x`y(l (pair ea eb))
|
||||
`a(a sp (unit ea)
|
||||
(l (pair ea eb)))))))
|
||||
|
||||
lam = `f(bind gns `v(bind f `e(unit (abstract v e))))
|
||||
|
||||
abs = Y `r`v`e(e `x`y(optimise (r v x) (r v y))
|
||||
`a(a v (atom i)
|
||||
(pair (atom k) (atom a)) ))
|
||||
|
||||
make = `x`y(pair (pair (atom s) x) y)
|
||||
|
||||
unopt = `a`b(pair (pair (atom s) a) b)
|
||||
|
||||
opt = `x(x `xx`xy(xx `xxx`xxy(make x)
|
||||
`xxa(xxa k `y(y `yx`yy(yx `yxx`yxy(make x y)
|
||||
`yxa(yxa k (pair (atom k) (pair xy yy))
|
||||
(make x y)))
|
||||
`ya(ya i xy (make x y)))
|
||||
(make x)))
|
||||
`xa(make x))
|
||||
|
||||
(Y `f(bind (bind trans pr) `i(f i)) I)
|
||||
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
--
|
||||
-- Haskell lambda and combinator utilities
|
||||
--
|
||||
|
||||
infixl 9 :@:
|
||||
|
||||
data Expr = Expr :@: Expr | Lambda String Expr | Var String
|
||||
| Y | I | J | K | S | C | B | SS | CC | BB
|
||||
| P | G | E Int
|
||||
deriving (Eq, Read, Show)
|
||||
|
||||
data EType = EFun | EArg | ELam deriving Eq
|
||||
|
||||
|
||||
isGraph c = c >= '!' && c <= '~'
|
||||
isToken c = isAlphanum c || '_' == c
|
||||
|
||||
disp e = display ELam e ""
|
||||
|
||||
exec e = do e' <- execute (compile (fst (parse e)))
|
||||
putStr (disp e')
|
||||
|
||||
comp = disp . compile . fst . parse
|
||||
|
||||
simp = disp . simplify . fst . parse
|
||||
|
||||
|
||||
|
||||
-- turn String into Expr
|
||||
|
||||
parse (a : as) | isSpace a = parse as
|
||||
| a == '`' = let (var, bs) = span isToken (dropWhile isSpace as)
|
||||
(expr, cs) = parse bs
|
||||
in (Lambda var expr, cs)
|
||||
| a == '(' = let (left, bs) = parse as
|
||||
fun left (c : cs) | isSpace c = fun left cs
|
||||
| c == ')' = (left, cs)
|
||||
| otherwise = let (right, ds) = parse (c:cs)
|
||||
in fun (left :@: right) ds
|
||||
in fun left bs
|
||||
| a == '\'' = case as of
|
||||
c:cs -> (E (ord c), cs)
|
||||
[] -> (E (-1), [])
|
||||
| isDigit a = let (bs, cs) = span isDigit as
|
||||
n = read (a:bs)
|
||||
in (E n, cs)
|
||||
| a == '-' = let (bs, cs) = span isDigit as
|
||||
n = read (if bs == "" then "1" else bs)
|
||||
in (E (-n), cs)
|
||||
| isToken a = let (bs, cs) = span isToken as
|
||||
in (case a:bs of
|
||||
"Y" -> Y; "I" -> I; "J" -> J; "K" -> K; "S" -> S; "C" -> C; "B" -> B
|
||||
"SS" -> SS; "CC" -> CC; "BB" -> BB; "P" -> P; "G" -> G; x -> Var x
|
||||
, cs)
|
||||
|
||||
|
||||
-- pretty printer
|
||||
|
||||
display t (Lambda v e) = showChar '`' . showString v . display ELam e
|
||||
display t (a :@: b) = showParen (t /= EFun) (display EFun a . showChar ' ' . display EArg b)
|
||||
display t (Var v) = showParen (t == ELam) (showString v)
|
||||
display t (E n) = let c = chr n in if isGraph c then showChar '\'' . showChar c else shows n
|
||||
display t e = showParen (t == ELam) (shows e)
|
||||
|
||||
|
||||
|
||||
-- translate into optimised combinators
|
||||
|
||||
compile (a :@: b) = compile a :@: compile b
|
||||
compile (Lambda var e) = abstract var (compile e)
|
||||
compile e = e
|
||||
|
||||
abstract v (a :@: b) = optimise (abstract v a) (abstract v b)
|
||||
abstract v e | e == Var v = I
|
||||
| otherwise = K :@: e
|
||||
|
||||
optimise (K :@: p) I = p
|
||||
optimise (K :@: p) (K :@: r) = K :@: ( p :@: r )
|
||||
optimise (K :@: p) (B :@: r :@: s) = BB :@: p :@: r :@: s
|
||||
optimise (K :@: p) r = B :@: p :@: r
|
||||
optimise (B :@: p :@: q) (K :@: r) = CC :@: p :@: q :@: r
|
||||
optimise p (K :@: r) = C :@: p :@: r
|
||||
optimise (B :@: p :@: q) r = SS :@: p :@: q :@: r
|
||||
optimise p r = S :@: p :@: r
|
||||
|
||||
|
||||
|
||||
-- do combinator reduction
|
||||
|
||||
execute ( Y :@: f) = let g = f :@: g in execute g
|
||||
execute ( I :@: f ) = execute f
|
||||
execute ( J :@: f :@: g) = execute g
|
||||
execute ( K :@: f :@: g ) = execute f
|
||||
execute ( S :@: f :@: g :@: x) = execute ((f :@: x) :@: (g :@: x))
|
||||
execute ( C :@: f :@: g :@: x ) = execute ((f :@: x) :@: g)
|
||||
execute ( B :@: f :@: g :@: x ) = execute (f :@: (g :@: x))
|
||||
execute (SS :@: c :@: f :@: g :@: x) = execute (c :@: (f :@: x) :@: (g :@: x))
|
||||
execute (CC :@: c :@: f :@: g :@: x ) = execute (c :@: (f :@: x) :@: g)
|
||||
execute (BB :@: c :@: f :@: g :@: x ) = execute (c :@: (f :@: (g :@: x)))
|
||||
|
||||
execute (G :@: f) = do c <- getChar
|
||||
execute (f :@: E (ord c))
|
||||
|
||||
execute (P :@: f :@: g) = do f' <- execute f
|
||||
case f' of
|
||||
E n -> do putChar (chr n)
|
||||
execute (I :@: g)
|
||||
_ -> return (f' :@: g)
|
||||
|
||||
execute (E n :@: f) = do f' <- execute f
|
||||
case f' of
|
||||
E m -> if n == m then return K else return J
|
||||
_ -> return (E n :@: f')
|
||||
|
||||
execute (f :@: g) = do f' <- execute f
|
||||
if f' == f then return (f' :@: g)
|
||||
else execute (f' :@: g)
|
||||
execute e = return e
|
||||
|
||||
|
||||
|
||||
-- translate into lambda calculus and do beta reduction
|
||||
|
||||
simplify I = fst (parse " `f f ")
|
||||
simplify J = fst (parse " `f`g g ")
|
||||
simplify K = fst (parse " `f`g f ")
|
||||
simplify S = fst (parse " `f`g`x ((f x) (g x)) ")
|
||||
simplify C = fst (parse " `f`g`x ((f x) g) ")
|
||||
simplify B = fst (parse " `f`g`x (f (g x)) ")
|
||||
simplify CC = fst (parse " `c`f`g`x (c (f x) g) ")
|
||||
simplify SS = fst (parse " `c`f`g`x (c (f x) (g x)) ")
|
||||
simplify BB = fst (parse " `c`f`g`x (c (f (g x))) ")
|
||||
|
||||
simplify (Lambda v b) = Lambda v (simplify b)
|
||||
|
||||
simplify (Lambda v b :@: a) = simplify (substitute v a b)
|
||||
|
||||
simplify (a :@: b) = let a' = simplify a
|
||||
b' = simplify b
|
||||
in if a' == a then (a' :@: b')
|
||||
else simplify (a' :@: b')
|
||||
simplify x = x
|
||||
|
||||
|
||||
|
||||
-- replace instances of variable v in body b with argument a, avoiding variable capture
|
||||
|
||||
substitute v a b = let wf b = newvar (merge (vars a) (vars b))
|
||||
subst (Var v') | v == v' = a
|
||||
| otherwise = Var v'
|
||||
subst (Lambda v' b) | v == v' = Lambda v' b
|
||||
| otherwise = let w = wf b in Lambda w (subst (substitute v' (Var w) b))
|
||||
subst (b :@: c) = (subst b) :@: (subst c)
|
||||
subst x = x
|
||||
in subst b
|
||||
|
||||
|
||||
|
||||
-- return a variable not in vs (which is sorted)
|
||||
|
||||
newvar vs = let x `isin` [] = False
|
||||
x `isin` (y:ys) | x < y = False
|
||||
| x == y = True
|
||||
| otherwise = x `isin` ys
|
||||
try v = if v `isin` vs then try (next v) else v
|
||||
next (v:vs) = if v < 'z' then (succ v):vs else 'a':(next vs)
|
||||
next [] = "a"
|
||||
in try "a"
|
||||
|
||||
|
||||
|
||||
-- get (sorted, unrepetitive) list of variables in an Expr
|
||||
|
||||
vars (Lambda v b) = merge [v] (vars b)
|
||||
vars (a :@: b) = merge (vars a) (vars b)
|
||||
vars (Var v) = [v]
|
||||
vars _ = []
|
||||
|
||||
|
||||
|
||||
-- combine two sorted lists, omitting duplicates
|
||||
|
||||
merge [] ys = ys
|
||||
merge xs [] = xs
|
||||
merge (x:xs) (y:ys) | x < y = x : merge (xs) (y:ys)
|
||||
| x == y = x : merge (xs) (ys)
|
||||
| otherwise = y : merge (x:xs) (ys)
|
||||
Reference in new issue
Block a user