Define the notion of "pairs" using higher-order logic

Question

Revising for a course on automated reasoning and I don't quite understand how to answer this question:

Show how the notion of pairs (x, y) can be defined in higher-order logic using a lambda abstraction. Define a function π1 that returns the first element of such a pair. Finally, show that π1(x, y) = x.

I've found similar questions on stackoverflow, but they're all to do with scheme, which I've never used. An explanation in English/relevant mathematical notation would be appreciated

Answer 1

Pairs or tuples describes Products Domain, is the union of all elements of the set A and all elements of the set B:

A × B = { (a, b) | a ∈ A, b ∈ B }

Here, A and B are diferent types, so if you for example are in a laguage program like C, Java, you can have pair like (String, Integer), (Char, Boolean), (Double, Double)

Now, the function π1, is just a function that takes a pair and returns the first element, this function is called in usually first, and that's how it looks like π1(x, y) = x, on the other hand you have second, doing the same thing but returning the second element:

fst(a, b) = a
snd(a, b) = b

When I studied the signature "Characteristics of the programming languages" in college our professor recommended this book, see the chapter Product Domain to understand well all this concepts.

Answer 2

The main topic of this question is to understand how data can be represented as functions. When you're working with other paradigms , the normal way of thinking is "data = something that's stored in a variable" (could be an array, object, whatever structure you want).

But when we're in functional programming, we can also represent data as functions. So let's say you want a function pair(x,y)

This is "pseudo" lisp language:

(function pair x y = 
   lambda(pick) 
      if pick = 1 return x 
      else return y  )

That example, is showing a function that returns a lambda function which expects a parameter.

(function pi this-is-pair = this-is-pair 1)

this-is-pair should be constructed with a pair function, therefore, the parameter is a function which expects other parameter (pick).

And now, you can test what you need

(pi (pair x y ) ) should return x

I would highly recommend you to see this video about compound data. Most of the examples are made on lisp, but it's great to understand a concept like that.

Answer 3

Here you go

PAIR := λx. λy. λp. p x y

π1 := λp. p (λx. λy. x)

π2 := λp. p (λx. λy. y)

π1 (PAIR a b) => a

π2 (PAIR a b) => b

Check the wiki entry on Church encoding for some good examples, too