[Kwartzlab CS] More on PRED
jonathan at jlamothe.net
Sat Mar 2 12:00:27 EST 2013
-----BEGIN PGP SIGNED MESSAGE-----
This makes sense, but I don't think we ever defined the EQ function.
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)
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