[Kwartzlab CS] More on PRED
jonathan at jlamothe.net
Sat Mar 2 12:03:03 EST 2013
-----BEGIN PGP SIGNED MESSAGE-----
... also, shouldn't it be:
Y (\f a n. EQ (SUCC a) n a (f (SUCC a) n)) (\s z. z)?
I believe the parens around the (f (SUCC a) n) are important.
On 13-03-02 12:00 PM, Jonathan Lamothe wrote:
> This makes sense, but I don't think we ever defined the EQ
> On 13-03-02 10:01 AM, Stephen Paul Weber wrote:
>> Now that we know about fixpoints, we could re-examine PRED if we
>> can define an operation for EQ. At least one such operation is
>> at <http://jwodder.freeshell.org/lambda.html>, but that
>> operation relies on PRED. For the purposes of this example let's
>> wave our hands and say that EQ is possible.
>> We are going to define a function which takes in two numbers.
>> If the sucessor of the first is equal to the second, return the
>> first. Otherwise, call ourselves on the successor. The idea here
>> is to "count up" until we are one less than the target, and then
>> return that number which is one less.
>> We then partially apply the outer layer to zero, so that we
>> count up starting at zero.
>> Y (\f.\a.\n. EQ (SUCC a) n a f (SUCC a) n ) (\s.\z. z)
> _______________________________________________ CS mailing list
> CS at kwartzlab.ca
PGP public key: http://www.jlamothe.net/keys/jonathan.asc
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/
-----END PGP SIGNATURE-----
More information about the CS