#StackBounty: #lambda-calculus #typed-lambda-calculus right way to define lambda-calculus konstruktors

Bounty: 50

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 konstruktor fst = λp. p (λa. λb. a) that returns the first element of the pair , we have now to define the snd konstruktor 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 konstruktors , how should man think when i have to define konstruktors, and how can i test that my answer is correct when im asked to define new konstruktors.

Get this bounty!!!

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.