Reputation: 709
I recently started studying Lambda Calculus as part of an assignment and I was tasked with writing a function for the logical operator >
, the syntax we are using is the same as shown in this video.
We are allowed to use basic math operations (+, -, /, *) and the equals operator (=) explicitly like so:
λx.λy.(x - y)
λx.λy.(x = y) TRUE FALSE
I found this website that explains it using less or equal to and comparing it against zero, the problem with this is that negative numbers are also different from zero.
Is there any way to write a Lambda Calculus function that works just like a GT operator like this?
I have tried substracting the first number from the second and then somehow dividing the result by itself so that I can get 1
if >
or a -1
if <
but I always end up with negative or positive for both <
and >
pairs of numbers.
Upvotes: 4
Views: 2079
Reputation: 106
If the numbers in mind are Church numerals them try:
lambda n: lambda m: isZero (m - n)
where:
isZero = lambda n: n (lambda _: False) True
(-) = lambda m: lambda n: m pred n
pred = λn.λf.λx. n (λg.λh. h (g f)) (λu.x) (λu.u)
(pred was from wikipedia)
Upvotes: 0
Reputation: 2127
The best I could come up with was either using only non-negative integers or allowing the square root operator.
If you don't have to use negative numbers, you can do this using recursion (with the Y-combinator) modeling the following function (using Python syntax):
def lt(x, y):
if y == 0:
return False
elif x == 0:
return y != 0
else:
return lt(x - 1, y - 1)
Since this isn't too bad, I'll let you figure out the application of the Y-combinator yourself. Feel free to comment if you have trouble.
If you have negative numbers, the best I can come up with is this. I won't be using the lambda calculus notation so you can convert these yourself:
ABS(x) = if (x == 0) then 0 else sqrt(x * x)
SIGN(x) = ABS(x) / (x + (x == 0))
LT(x, y) = (-1 == SIGN(x - y))
Note: I am taking the liberty in having boolean expressions return the integers 1
or 0
instead of the functions TRUE
or FALSE
, as in the Collected Lambdas link you posted. If this is a problem, you can write a function that maps TRUE
to 1
and FALSE
to 0
.
If you look at just the last equation for LT
, it's pretty clear why it works. You first compute x - y
. Then, you take the sign of that expression. The sign of x - y
if -1
iff x < y
is true.
The explanation for SIGN
is that, when x == 0
, we'll have the expression 0/1
, which is correct. If x != 0
, then we'll have |x|/x
, which will be -1
or 1
depending on the sign of x
.
Upvotes: 1