Re: [stack] New on Joy page: "Church arithmetic and Church logic"
Brent Kerby — 2002-10-09 07:18:24
Thanks, Manfred, for that nice page on Church numbers in Joy. Here's a few
observations that might be of some use ...
About the construction of Csucc (which adds one to a church number),
Csucc == [dup [i] dip] dip i.
this can be simplified a bit:
Csucc == [dup dip] dip i.
becuase "dup [i] dip" is the same as "dup dip"; by the way, the "dup dip"
combinator is an interesting one; I call it "run", since it in effect
executes a program without destroying the program.
----------
Anyhow, onto the next construction:
Cadd == [ [[Csucc] cons] ] dip i i;
Here's an alternative:
Cadd == [sip] dip i
It works like this:
[p] [m] [n] [sip] dip i
== [p] [m] sip [n] i
== [p] m [p] [n] i
== [p] m [p] n
------------
Next,
Cmul == [ [[C0]] dip [Cadd] cons [cons] cons ] dip i i;
An alternative:
Cmul == [cons] dip i
It works like this:
[p] [m] [n] [cons] dip i
== [p] [m] cons [n] i
== [[p] m] n
-----------------
Finally,
Cpow == [ [[C1]] dip [Cmul] cons [cons] cons ] dip i i.
And, an alternative:
Cpow == [[cons] cons] dip i i
Working like this:
[p] [m] [n] [[cons] cons] dip i i
== [p] [m] [cons] cons n i
== [p] [[m] cons] n i
== [[[[[p] m] m] m] ...] i
Unfortunately, in this system of church numbers, the Cpow is not a true
combinator, only a pseudo-combinator (unlike Csucc, Cadd, and Cmul, which
are true combinators).
----------------
By the way, there are several other ways of doing church numbers in Joy. The
current way assumes,
[p] Cn == p p ... p
But alternatively we could do:
[p] Rn == p p ... p [p]
The only difference here is that we save the original program "p". The
principle advantage of this approach is that then Rn are reversible
combinators (note, Cn were all irreversible combinators since they destroy
the original program). We'd have,
R0 ==
R1 == run
R2 == run run
R3 == run run run
...
This is quite an elegant setup, seeing that simply "run" acts as a successor
function, and C0 is simply the empty program. Also, the negative church
numbers then are
R-1 == unrun
R-2 == unrun unrun
R-3 == unrun unrun unrun
...
Note the reverse of any church number then is simply its negative. Also, to
add church numbers is simply to concatenate them. Of course, "cat" itself is
irreversible, so we might use "rat":
[b] [a] rat == [b a] [a]
This is a suitable addition function for the Rn church numbers; notice it
preserves one of the parameters, like a reversible addition function should.
Also, unlike Cadd, it does not execute the newly formed program (doing so
would be irreversible, as "i" is irreversible).
Here's how to multiply these Rn church numbers:
Rmul == swap cons untack
It works, for example, like this:
[2] [3] swap cons untack
== [[3] 2] untack
== [3 3 [3]] untack
== [3 3] [3]
== [6] [3]
So that's nice, except that this is not really reversible, since "cons" is
not reversible (assuming we have transparent quotation; if we have opaque
quotation then "cons" is reversible, but the multiplication then doesn't
work because "untack" fails):
[a] [dup] cons == [[a] dup] == [[a] [a]]
[[a] [a]] [] cons == [[a] [a]]
See how cons can give the same result from different inputs? This means it
is irreversible.
So can Rmul be defined from reversible primitives? If so, we would expect to
fail in the case of multiplying by zero, since that is irreversible. Also,
having a reversible Rmul would give us the ability to do division, and the
ability to construct fractional church numbers. But do fractional church
numbers make sense? For example, the church number for 1/2 would have the
rule:
[a a] R1/2 == a [a a]
In a system with transparent quotation, it seems like R1/2 would not be
straightforward to implement, perhaps impossible, since it would require the
system to try to coerce an arbitrary "[p]" into the form "[a a]", by using
reductions and expansions inside the quotation. But maybe there is some
reasonable way to do it ...
- Brent
Manfred von Thun — 2002-10-09 09:08:09
Thanks for that. You do not cease to amaze me.
It is too late today to do full justice to your contribution,
except for one question that immediately occurred to me.
On Wed, 9 Oct 2002, Brent Kerby wrote:
[..deleted lots of much improved definitions for Church arithmetic..]
> Finally,
>
> Cpow == [ [[C1]] dip [Cmul] cons [cons] cons ] dip i i.
>
> And, an alternative:
>
> Cpow == [[cons] cons] dip i i
>
> Working like this:
>
> [p] [m] [n] [[cons] cons] dip i i
> == [p] [m] [cons] cons n i
> == [p] [[m] cons] n i
> == [[[[[p] m] m] m] ...] i
>
> Unfortunately, in this system of church numbers, the Cpow is not a true
> combinator, only a pseudo-combinator (unlike Csucc, Cadd, and Cmul, which
> are true combinators).
Could you clarify why you say that your Cpow is not a true combinator?
I have often thought that there are all sorts of possible
classifications of combinators (e.g. I have tried to find
second order combinators that are not also useable as first
order combinators, but I have now concluded that there are none).
You are pointing to a distinction (true / false?mock?pseudo?)
which I do not understand but which might be of interest more
generally.
I do remember that in one reference (I cannot remember which, alas)
it was pointed out that exponentiation could be implemented
as applying the exponent n to the base m, but that was
considered "cheating" [sic]. I did not understand that
either, but maybe you are talking about the same thing.
[..deleted material on reversible Church-like numerals..]
> - Brent
Thanks again for your long contribution. I hope to come
back to it soon.
- Manfred
Manfred von Thun — 2002-10-21 07:24:20
On Wed, 9 Oct 2002, Brent Kerby wrote:
> Thanks, Manfred, for that nice page on Church numbers in Joy. Here's a few
> observations that might be of some use ...
I'm finally getting around to doing a tiny bit outside my current
teaching. Thanks again for this long contribution.
It would be a great shame if your elegant alternatives to my
Church numerals did get buried in the concatenative group.
There seem to be several possibilities:
1. At the end of my Church numeral page I plant a link
to your concatenative article.
2. I copy your article to the Joy page, properly
acknowledged. At the end of my Church numeral page
I plant a link to that article.
3. I add your article as it is, properly acknowledged,
to the end of my Church numeral page.
4. One of us, you or I, writes tests for your alternatives
to incorporate as for (3).
Choices 1 2 3 would only need your consent and decision, but
choice 4 would need some work:
a) for the test file jp-church.joy
b) for the text file jp-church.html
Do you have any views, opinions, preferences ?
[...]
> Unfortunately, in this system of church numbers, the Cpow is not a true
> combinator, only a pseudo-combinator (unlike Csucc, Cadd, and Cmul,
which
> are true combinators).
I asked about "true combinators" earlier, thanks for the explanation
you gave so quickly.
[...]
> By the way, there are several other ways of doing church numbers in Joy. The
> current way assumes,
>
> [p] Cn == p p ... p
>
> But alternatively we could do:
>
> [p] Rn == p p ... p [p]
>
> The only difference here is that we save the original program "p". The
> principle advantage of this approach is that then Rn are reversible
> combinators (note, Cn were all irreversible combinators since they destroy
> the original program).
We would also need to discuss whether your material on reversibe
Church numbers should be included or whether it should be treated
as a separate topic.
[...]
- Manfred
Brent Kerby — 2002-10-23 05:57:45
> It would be a great shame if your elegant alternatives to my
> Church numerals did get buried in the concatenative group.
> There seem to be several possibilities:
>
> [...]
I'd have no problem if you pasted it at the end of you Church numeral's
page; whatever you'd like to do with it is quite fine with me, actually.
> > [p] Cn == p p ... p
> >
> > But alternatively we could do:
> >
> > [p] Rn == p p ... p [p]
> >
> > [...]
>
> We would also need to discuss whether your material on reversibe
> Church numbers should be included or whether it should be treated
> as a separate topic.
It seems like it'd make sense though to go ahead and include the information
on the reversible "Rn" church numbers (maybe also along with the "Zn" church
numbers) at the end of the article. But then again, whatever seems best to
you is fine with me.
> - Manfred
- Brent
Manfred von Thun — 2002-10-25 06:09:27
On Wed, 23 Oct 2002, Brent Kerby wrote:
> I'd have no problem if you pasted it at the end of you Church numeral's
> page; whatever you'd like to do with it is quite fine with me, actually.
Done
> It seems like it'd make sense though to go ahead and include the information
> on the reversible "Rn" church numbers
Done
(maybe also along with the "Zn" church
> numbers) at the end of the article.
Done
Thank you very much again.
- Manfred