about

# Church Pairs

## 10.12.2019

Using Church boolean encodings we can encode pairs. On pairs we have projections, normally called $fst$ and $snd$ for first and second element of the pair, respectively. We create a pair as $$\lambda f .\ \lambda s .\ \lambda b .\ b\ f\ s$$ note here that if we bind $f$ and $s$ to two terms, we can access them binding $true$ respectively $false$ to $b$. Thus we get $$fst = \lambda p .\ p\ true$$ $$snd = \lambda p .\ p\ false$$

That is it. You can experiment here:

// literals let true = \ t . \ f . t; let false = \ t . \ f . f; // operators let pair = \ f . \ s . \ b . b f s; let fst = \ p . p true; let snd = \ p . p false; // conditional let test = \ l . \ m . \ n . l m n; // evaluation fst (pair one two)

...

CommentsGuest Name:Comment: