Looking for a Church-encoding (lambda calculus) to define < , > , !=

Question

I have to create some Lambda functions for > , < and !=

I don't have an idea how to , could anyone help me please ? PS: We just started with Lambda Calculus, so please do not assume any previous knowledge.

Thank you in anticipation !

Edit - What I meant was Arithmetic in Lambda Calculus

Edit 2 - More accurate : Looking for a Church-encoding (lambda calculus) to define < , > , !=

---

Editor's Note: I think this is what the OP is trying to ask:

I am trying to implement the following operations in the untyped lambda calculus using Church encoding:

1. Greater than (GT or >).
2. Lesser than (LT or <).
3. Not equal to (NE or !=).

I already know how to implement the following:

1. Boolean true (TRUE or λx.λy.x).
2. Boolean false (FALSE or λx.λy.y).
3. Logical and (AND or λp.λq.p q p).
4. Logical or (OR or λp.λq.p p q).
5. Logical not (NOT or λp.λa.λb.p b a).

How would you write the GT, LT and NE functions in the untyped lambda calculus?

Answer 1

You also need the implementation of natural numbers. That's what you're going to write comparision operators for, isn't it.

I think that I remember the implementation of natural numbers. A number n is represented as a function taking a function f and a value x, and applying f n times on x.

zero = λf . λx . x
succ = λn . λf . λx . n f (f x)

Answer 2

Using "An Introduction To Functional Programming Through Lambda Calculus" by Greg Michaelson

Starting with

Section 4.8.3. Comparison

There are a number of ways of defining equality between numbers. One approach is to notice that the difference between two equal numbers is zero. However, if we subtract a number from a smaller number we also get zero so we need to find the absolute difference between them; the difference regardless of the order of comparison. To find the absolute difference between two numbers, add the difference between the first and the second to the difference between the second and the first:

def abs_diff x y = add (sub x y) (sub y x)

If they are both the same then the absolute differences will be zero because the result of taking each from the other will be zero. If the first is greater than the second then the absolute difference will be the first minus the second because the second minus the first will be zero. Similarly, if the second is greater than the first then the difference will be the second minus the first because the first minus the second will be zero.

Thus, we can define:

def equal x y = iszero (abs_diff x y)

We can also use subtraction to define arithmetic inequalities. For example, a number is greater than another if subtracting the second from the first gives a non-zero result:

def greater x y = not (iszero (sub x y))

Less is defined in the solutions to exercises section in the back.

def less x y = greater y x

Now using the book in the link just find all of the subordinate functions and you will have =, >, <. While the book does not define != it should be obvious.

EDIT

Per comment by WillNess

4.8.2. Subtraction

To find the difference between two numbers, find the difference between the numbers after decrementing both. The difference between a number and zero is the number:

rec sub x y =
if iszero y
then x
else sub (pred x) (pred y)

Please note "Now using the book in the link just find all of the subordinate functions".

I don't plan on hunting down all of the subordinate functions and listing them here because they would explode into recreating many functions here. I have read and worked through portions of the book and it is comprehensive enough that I was not lacking for info.

Answer 3

The Wikipedia article on Church encoding has a section on predicates that covers EQ and LEQ