9
votes

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?

3
What does "create lambda function for >" mean? A lambda that just wraps the operator? What on earth would be the point of that?Sebastian Redl
@SebastianRedl: The OP seems to be (sorry if I'm wrong) not very used to haskell and might not know that <, > and /= are just normal functions.Kritzefitz
So basically, he might just want the section (<), which can be used as a normal function.Sebastian Redl
We don't know what he wants.augustss
@user2938633 Oh we know what a lambda is, thank you very much. But what the hell are you asking?Bartek Banachewicz

3 Answers

4
votes

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.

2
votes

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)
1
votes

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