# 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