comments - 7
phimvt@lurac.latrobe.edu.au — 2000-08-02 03:30:52
I'm still a long way behind, sorry - Manfred
1. "Joy in Avail"
This was an impressive sequence of contributions: Mark's Joy in
Avail, and Stevan's Joy on K. I had looked briefly at K before,
and I did now have a look at the Avail web page.
I only had one nagging question about Stevan's K version:
The definitions look like e.g.
shunt : I"[swons] step"
Never mind the colon instead of ==. But do the I and the two double
quotes mean that the body of this definition is stored as a string
of characters which has to be rescanned character by character every
time the shunt function is called? Of course if one does not care
about efficiency and only wants an in-principle implementation,
then this does not matter. On the other hand, if one wants efficiency
(though still interpreted), then the body should be a list of two
items, where the first item is again a list, of only one item.
There are many ways of implementing languages - depending in
part on how close the implementation is to the definition of the
language, and also on how close the implementation language is.
Here is a rough scale (using Joy as the example):
a) Write a complete scanner, parser, (type-checker,) and interpreter
in any old general purpose programming language (e.g. my Joy prototype
in C, also two earlier versions in Pascal).
b) Use the scanner and parser of the implementation language,
just write the interpreter. If the implementing language is Lisp,
just use Lisp's round parentheses instead of Joy's square brackets
- and put up with the difference. If the implementing language is
Prolog, lists are already in square brackets but list items have
to be separated by commas - put up with that.
c) Be satisfied with a very different syntax altogether, just
implement the functionality. This of course misses out on one central
feature of Joy:
The function denoted by the concatenation of programs is
is the composition of the functions denoted by those programs.
This can still be very useful if the implementation has some
special merits. To combine the above feature and the merits,
one then has to write a (presumably very simple) compiler
from Joy syntax to the very different syntax of the implementation.
In the same thread there was again mention of continuations.
I have commented on the topic before, but I still have not yet been
able to study the Lispkit book by Henderson again. I should mention
this, though: continuations are by no means restricted to functional
languages. In (proper) implementations of Pascal it is possible
to have recursive procedures which take as a parameter a local
procedure which will access the initial parameters of the recursive
procedure (are you still with me?). I have used this a lot to
implement backtracking in Pascal. It is always very hard to convince
students that one cannot do it in C, and I have yet to see a
P2C translator that can handle it.
2. "Joy combinator construction"
Brent Kirby wrote an impressive theorem prover for Joy algebra.
Fantastic! With some (minor?) changes it could well work as a optimiser
for the day when Joy has to be used for real-life programming.
The result: "dip cannot be defined in terms of other primitives"
I had known (well, sort of conjectured) before. But I hope Brent
continues work on that theorem prover. Has anyone thought of doing
that sort of thing in Prolog?
Brent also referred to the early literature on combinatory logic,
and raised the question of what the precise relationship with Joy is.
It will not surprise you that Joy took a lot of inspiration from
that early work on combinators (see my paper "Joy compared with
other functional languages").
Combinatory logic only needs the two combinators S and K,
and one could give precise Joy counterparts which I'll call s and k.
We require a translation from combinatory calculus to Joy. Constants
translate as themselves. Given a combinatory expression x, let 'x
be its translation into Joy. The reduction rule for K (in prefix)
requires that 'y ['x] k (in Joy postfix) reduces to 'x. The reduction
rule for S requires that 'x ['g] ['f] s reduces to 'x 'g 'x 'f.
The two Joy combinators s and k could then be the sole basis.
Alternatively, they might be defined in terms of more familiar
primitives:
k == [pop] dip i
s == [[dup] dip i swap] dip i
(unless I have made a mistake). Maybe Brent's theorem prover should
be set to work on this. The point of it all is that with just s and k
we have Turing completeness.
iepos@tunes.org — 2000-08-04 15:11:13
> 2. "Joy combinator construction"
> Brent Kirby wrote an impressive theorem prover for Joy algebra.
> Fantastic! With some (minor?) changes it could well work as a optimiser
> for the day when Joy has to be used for real-life programming.
> The result: "dip cannot be defined in terms of other primitives"
> I had known (well, sort of conjectured) before.
Well, it can be constructed as "swap unit concat i".
> But I hope Brent continues work on that theorem prover. Has anyone
> thought of doing that sort of thing in Prolog?
I don't know Prolog. But it surely is tedious doing it how I have in C.
Prolog probably would be a better choice.
> Combinatory logic only needs the two combinators S and K,
> and one could give precise Joy counterparts which I'll call s and k.
> We require a translation from combinatory calculus to Joy. Constants
> translate as themselves. Given a combinatory expression x, let 'x
> be its translation into Joy. The reduction rule for K (in prefix)
> requires that 'y ['x] k (in Joy postfix) reduces to 'x. The reduction
> rule for S requires that 'x ['g] ['f] s reduces to 'x 'g 'x 'f.
> The two Joy combinators s and k could then be the sole basis.
This is interesting. I had not realized yet that there was complete
two-combinator base in Joy. I don't think your "s" and "k" quite work,
because there is no way to get a cons'ing effect. However, if we modify
your "s" a bit to do some quotation, I think it would work:
[y] [x] k -> x
[z] [y] [x] s -> [[z] y] [z] x
We can construct "i" then as "[k][k]s", as we'd expect from traditional
combinatory logic:
[x] [k] [k] s
[[x] k] [x] k
x
In general, "[foo][k]s" or even "1[k]s" would work.
We can construct the analogue of the B combinator as "[k][[s]k]s":
[z] [y] [x] [k] [[s] k] s
[z] [y] [[x] k] [x] [s] k
[z] [y] [[x] k] s
[[z] y] [z] [x] k
[[z] y] x
The analogue of the C combinator as "[[k]k][[s][b]b]s" I think
("b" in the sense above, not the "b" as in the Joy system):
[z] [y] [x] c -> [y] [z] x
From that we could construct swap as "[] c". This is interesting.
I wonder how "dip" might be constructed... Perhaps this would be an
interesting job for the little construction-finder, as you've suggested.
It appears promising that we do have a complete base.
- "iepos" (Brent Kerby)