IvanHid
IvanHid

Reputation: 709

Lambda Calculus exfunction for Greater Than ">"

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

Answers (2)

Brian Duong
Brian Duong

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

Enrico Borba
Enrico Borba

Reputation: 2127

Preface

The best I could come up with was either using only non-negative integers or allowing the square root operator.

Without Negative Integers

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.

With Negative Integers and The Square Root Operator

Definition

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.

Explanation

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

Related Questions