Extending Church Numerals to integers, rationals
Tim Sweeney
natural numbers?
Church Numerals are a convenient way of encoding natural numbers in
the lambda calculus. A Church Numeral N is a function that, given a
function F as input, returns F iterated N times. In other words:
0 = lambda(f).lambda(x).x
1 = lambda(f).lambda(x).f(x)
2 = lambda(f).lambda(x).f(f(x))
n+1 = lambda(f).lambda(x).f(n(f)(x))
Church Numerals are interesting because they admit a very simple
representation of addition, multiplication, and exponentiation:
a+b = lambda(f).a(f)(b(f))
a*b = lambda(f).a(b(f))
a^b = lambda(f).lambda(g).g(f)
In this spirit, we can write computationally valid (though perhaps
mathematically odd-sounding) expressions such as:
sin*cos (x) = sin(cos(x))
sin^3 (x) = sin(sin(sin(x)))
One can imagine extending Church Numerals (as entities of the lambda
calculus) beyond the natural numbers in an analogous way to extending
the natural numbers to the integers, rationals, or reals: just as "2"
is a function that iterates its argument twice, "-1" is a function
that returns the inverse of its argument.
I'm intentionally oversimplifying, of course: such an "inverter"
function only makes sense when its argument is a function with a valid
inverse, but that does not necessarily invalidate the concept. Such a
condition of invertability could perhaps be expressed in a
sufficiently powerful dependent-typed lambda calculus.
I'm interested in any pointers to research along these lines because
this seems like it may be a fruitful way of extending well-known
mathematical concepts (such as addition, multiplication, and
exponentiation) into functional concepts, in a well-defined way.
-Tim
Chas Brown
Tim Sweeney wrote:
>
> Does anybody know of work on extensions of Church Numerals beyond the
> natural numbers?
>
> Church Numerals are a convenient way of encoding natural numbers in
> the lambda calculus. A Church Numeral N is a function that, given a
> function F as input, returns F iterated N times. In other words:
>
> 0 = lambda(f).lambda(x).x
> 1 = lambda(f).lambda(x).f(x)
> 2 = lambda(f).lambda(x).f(f(x))
> n+1 = lambda(f).lambda(x).f(n(f)(x))
>
> a*b = lambda(f).a(b(f))
> a^b = lambda(f).lambda(g).g(f)
<snip>
> I'm intentionally oversimplifying, of course: such an "inverter"
> function only makes sense when its argument is a function with a valid
> inverse, but that does not necessarily invalidate the concept.
Interesting idea. Just talking out of my hat, I'd say...
Given the above restriction (which basically seems to restrict the set
of functions acted upon to a group under composition), I can see how one
could build a structure which is ring-isomorphic to Z
But I don't see how to additionally restrict the set of functions acted
upon so as to guarantee the existence of a _multiplicative_ inverse -
i.e., an element a' of the lambda calculus such that a'*a = a*a' = 1.
Does a^-1 as defined above do the job?
Alternatively, you could create equivalence classes of Church Numeral
pairs [p,q]; defining (p,q)~(p',q') if there exists some non-0 Church
Numerals m and n such that (m*p, m*q) = (n*p', n*q'); and then proceed
as usual with operations defined as:
[p,q] + [p',q'] = [p*q' + p'*q, q*q']
[p,q] * [p',q'] = [p*p', q*q']
to at least get a structure that resembles Q as a field.
Cheers - Chas
Torben Ægidius Mogensen
> Does anybody know of work on extensions of Church Numerals beyond the
> natural numbers?
>
> Church Numerals are a convenient way of encoding natural numbers in
> the lambda calculus. A Church Numeral N is a function that, given a
> function F as input, returns F iterated N times. In other words:
>
> 0 = lambda(f).lambda(x).x
> 1 = lambda(f).lambda(x).f(x)
> 2 = lambda(f).lambda(x).f(f(x))
> n+1 = lambda(f).lambda(x).f(n(f)(x))
>
> Church Numerals are interesting because they admit a very simple
> representation of addition, multiplication, and exponentiation:
>
> a+b = lambda(f).a(f)(b(f))
> a*b = lambda(f).a(b(f))
> a^b = lambda(f).lambda(g).g(f)
>
> In this spirit, we can write computationally valid (though perhaps
> mathematically odd-sounding) expressions such as:
>
> sin*cos (x) = sin(cos(x))
> sin^3 (x) = sin(sin(sin(x)))
I can't see how this follows.
>
> One can imagine extending Church Numerals (as entities of the lambda
> calculus) beyond the natural numbers in an analogous way to extending
> the natural numbers to the integers, rationals, or reals: just as "2"
> is a function that iterates its argument twice, "-1" is a function
> that returns the inverse of its argument.
>
> I'm intentionally oversimplifying, of course: such an "inverter"
> function only makes sense when its argument is a function with a valid
> inverse, but that does not necessarily invalidate the concept. Such a
> condition of invertability could perhaps be expressed in a
> sufficiently powerful dependent-typed lambda calculus.
>
> I'm interested in any pointers to research along these lines because
> this seems like it may be a fruitful way of extending well-known
> mathematical concepts (such as addition, multiplication, and
> exponentiation) into functional concepts, in a well-defined way.
My paper "An Investigation of compact and efficient number
representations in the pure lambda calculus" (Springer LNCS 2244)
shows how to represent integers in lambda calculus using balanced
ternary notation. This gives more compact representation than
Church-numerals and more efficient operations. The operations are
more complicated, though.
Torben Mogensen (tor...@diku.dk)
Vidhyanath Rao
"Tim Sweeney" <t...@epicgames.com> wrote in message
news:9ef8dc7.02071...@posting.google.com...
> [...]
> sin*cos (x) = sin(cos(x))
> sin^3 (x) = sin(sin(sin(x)))
The first is usually denoted by a little circle (for composition); the
second is avoided for number-values functions, but used in contexts
where values of functions have no exponentiation.
> One can imagine extending Church Numerals (as entities of the lambda
> calculus) beyond the natural numbers in an analogous way to extending
> the natural numbers to the integers, rationals, or reals: just as "2"
> is a function that iterates its argument twice, "-1" is a function
> that returns the inverse of its argument.
This kind of thing is used when dealing with groups: Natural numbers act
on any monoid, using the same approach in Church numerals. Integers act
on any group. Groups localized at some primes or at rationals (so that
you can define suitable fractional powers) have been in use for decades.
Further extensions have occassionally made their appearance, but I don't
know of systematic investigations.
Combining the above with lambda calculus, I have no idea. You will need
to come up with suitable models which have the appropriate structure.
William Elliot
> Church Numerals are a convenient way of encoding natural numbers in
> the lambda calculus. A Church Numeral N is a function that, given a
> function F as input, returns F iterated N times. In other words:
>
> 0 = lambda(f).lambda(x).x
> 1 = lambda(f).lambda(x).f(x)
> 2 = lambda(f).lambda(x).f(f(x))
> n+1 = lambda(f).lambda(x).f(n(f)(x))
>
> a+b = lambda(f).a(f)(b(f))
> a*b = lambda(f).a(b(f))
> a^b = lambda(f).lambda(g).g(f)
>
Are you sure about a^b as presented?
>"-1" is a function that returns the inverse of its argument.
>
(-1)ff = I = (lam x)x; (lam f)(lam f)I, does that.
So (-1)f = 0; (lam f) 0, does that.
-----= Posted via Newsfeeds.Com, Uncensored Usenet News =-----
http://www.newsfeeds.com - The #1 Newsgroup Service in the World!
-----== Over 80,000 Newsgroups - 16 Different Servers! =-----
Tom Breton
> Does anybody know of work on extensions of Church Numerals beyond the
> natural numbers?
[snip excellent summary of Church Numerals]
> One can imagine extending Church Numerals (as entities of the lambda
> calculus) beyond the natural numbers in an analogous way to extending
> the natural numbers to the integers, rationals, or reals: just as "2"
> is a function that iterates its argument twice, "-1" is a function
> that returns the inverse of its argument.
>
> I'm intentionally oversimplifying, of course: such an "inverter"
> function only makes sense when its argument is a function with a valid
> inverse, but that does not necessarily invalidate the concept. Such a
> condition of invertability could perhaps be expressed in a
> sufficiently powerful dependent-typed lambda calculus.
>
> I'm interested in any pointers to research along these lines because
> this seems like it may be a fruitful way of extending well-known
> mathematical concepts (such as addition, multiplication, and
> exponentiation) into functional concepts, in a well-defined way.
No pointers, but it seems to mirror the difference between ordinary
functional programming and logic programming (Prolog, Mercury). In
logic languages a parameter may be "-" or "+", ie, given or found.
Which is to say, their rules can produce answers both of the form
y = f(x)
and of the form
y such that f(y) = x
The second seems to be essentially what your inverter does. Both are
basically implicit equations.
Which is not to say that the concept would actually make sense in any
logic language. Some (LambdaProlog, Mercury) do have lambda, but it
means something different.
BTW, long time no see! How have you been?
--
Tom Breton at panix.com, username tehom. http://www.panix.com/~tehom
William Lovas
> On 16 Jul 2002, Tim Sweeney wrote:
>
>> a+b = lambda(f).a(f)(b(f))
>> a*b = lambda(f).a(b(f))
>> a^b = lambda(f).lambda(g).g(f)
>>
> Are you sure about a^b as presented?
This is by no means a proof, but some quick testing in O'Caml supports
the conjecture:
let c2 = fun s z -> s (s z);;
let c3 = fun s z -> s (s (s z));;
let exp m n = n m;;
(* to convert a church numeral to an integer representation, *
* we pass along an integer representation of `succ' and `0' *)
let int_of_churchnat n = n succ 0;;
(* then in the toplevel *)
# int_of_churchnat (exp c2 c3);;
- : int = 8
# int_of_churchnat (exp c3 c2);;
- : int = 9
# int_of_churchnat (exp c3 c3);;
- : int = 27
It's also covered in plenty of textbooks and lecture notes; i'm convinced :)
What i'd like to know is just what is Epic Megagames working on these days
that requires so much theoretical computer science? :P
William, whose first exposure to computer games was ZZT. . .
ol...@pobox.com
> Does anybody know of work on extensions of Church Numerals beyond the
> natural numbers?
The following page
http://pobox.com/~oleg/ftp/Computation/Computation.html#lambda-calc-neg
specifically deals with negative numbers, subtraction, and division in
Lambda Calculus. In particular,
http://pobox.com/~oleg/ftp/Computation/lambda-arithm-div-term.scm
is the lambda term that performs division of two signed integers. An
article referred to on the first page describes how this term was
derived. See also
http://www.mail-archive.com/has...@haskell.org/msg10769.html
for a lambda-interpreter in Haskell and examples of negative numbers
and comparisons.
Tim Sweeney
take a short break from game programming and work on an interesting
side-project. Currently I'm fascinated with the applications of type
theory, and am experimenting with extensions that increase
expressiveness at the expense of decidable typechecking and possibly
even reduction.
Regarding Church Numerals, another thought along these lines is to
extend the lambda calculus with a new primitive "-1", not itself
definable as a finite lambda term, and define a new (possibly
incomplete) reduction rule for it which captures the essence of a
negative church numeral: that for all terms f and x,
f(-1(f)(x))=-1(f)(f(x))=id.
It was mentioned that -1 is the fixed point of y=y+y+1, but that leads
to an infinite expansion that does not appear to be computationally
useful.
It is interesting to restate a problem such as "y such that f(y) = x",
as -1(f)(x). Not that this causes a solution to magically appear!
But it does move the problem from solving an equation to evaluating an
expression in a lambda calculus augumented with the primitive "-1".
The notion of negative Church Numeral terms makes varying degrees of
sense in different calculi. It is most interesting in a logic
programming framework supporting terms with multiple "potential"
values such as McAllester's Ontic: http://www.autoreason.com/. In
this sort of framework, it seems that every function has a unique and
perfectly sensible (though possibly multivalued, and not necessarily
computable) inverse.
Regarding exponentiation ("a^b = lambda(f).lambda(g).g(f)"), this
agrees with convention for all natural numbers, except for the
somewhat questionable case of 0^0=0.
[Disclaimer: I'm presenting this experimentally and have not attempted
to prove the soundness of the proposed extensions.]
William Elliot
_ Regarding exponentiation ("a^b = lambda(f).lambda(g).g(f)"), this
_ agrees with convention for all natural numbers, except for the
_ somewhat questionable case of 0^0=0.
But then, a^b = lambda(f).lambda(g).g(f) = n^m. What gives?
----