Right way to define lambda-calculus constructors

Question

Is there a clear way to find terms in lambda-calculus? For example assume that we have a pair constructor

pair = λa. λb. λf. f a b

and we have the fst constructor

fst = λp. p (λa. λb. a)

that returns the first element of the pair , we have now to define the snd constructor which returns the second item of the pair. I have arrived to define it like this

snd = λp. p (λa. λb. b) with snd (pair a b) = b.

snd can be defined also as

snd = λp. p (λb. λa. b) ,

the question is, is there a clear way how to define new constructors?

How should man think when I have to define constructors, and how can I test that my answer is correct when I'm asked to define new constructors.

Answer 1

(λa. (λb. b)) x y = (λb. b) y = y

but

(λb. (λa. b)) x y = (λa. x) y = x

, so no, the two are not equivalent: the first definition returns its second argument, but the second definition returns its first argument.

Names do not count, except for establishing the correspondence with the arguments. Arguments' positions count.

As to how to think about it, I often find writing the definitions down in the combinatory style much easier to follow:

pair a b selector = selector a b

fst apair = apair first_argument_selector

snd apair = apair second_argument_selector

first_argument_selector  a b = a

second_argument_selector a b = b

I think this is very clear. "A pair of a and b will, given a selector procedure, feed it a first, and b, second." etc.

We can go back and forth between the two styles with simple syntactic transformations, e.g.:

second_argument_selector     a     b = b       =>
second_argument_selector     a = (λb . b)      =>
second_argument_selector = (λa . (λb . b))

The principle of wishful thinking is often very helpful: we use some functions as if they were already written; then their uses dictate us how they must be defined. Just like we did with the first_argument_selector and second_argument_selector, above.

Good names help. Visually aligning the code helps. Also, using full parenthesization (like I did at the top of the post).