<p>I am looking for references for a notion of Böhm tree for the λ-calculus with pairs and projections (and the reduction rule <span class="math-container">$\pi_i\, \langle t_1, t_2\rangle \longrightarrow t_i$</span>).
I'm only aware of <a href="https://www.cs.ox.ac.uk/andrzej.murawski/papers/popl18.pdf" rel="noreferrer">this POPL'18 paper</a> that gives a definition for linearly typed λ-terms with fixpoints (Y) and additive product types (&amp;). Since the idea seems natural even in an untyped setting, I'd expect older references to exist, but I have not managed to find any…</p>

CC BY-SA 4.0
2024-05-17T13:31:35.610Z
Papers about the "lambda calculus with constructors" might be relevant. And you can also try using a keyword that relates to the possibility of error states (since you now have functions and pairs, but no types to prevent cross interactions), e.g. "error", "clash", or "daimon".
xavierm02
CC BY-SA 4.0
2024-05-17T14:43:32.557Z
Papers that cite "The virtues of eta-expansion" might also be relevant
xavierm02
<reference-request><lambda-calculus>
Böhm tree with pairs (product types)
Lê Thành Dũng 'Tito' Nguyễn
# Böhm tree with pairs (product types)

(Asked by: username_0 on 2024-05-03)

I am looking for references for a notion of Böhm tree for the λ-calculus with pairs and projections (and the reduction rule $\pi\_i\, \langle t\_1, t\_2\rangle \longrightarrow t\_i$).
I'm only aware of [this POPL'18 paper](https://www.cs.ox.ac.uk/andrzej.murawski/papers/popl18.pdf) that gives a definition for linearly typed λ-terms with fixpoints (Y) and additive product types (&). Since the idea seems natural even in an untyped setting, I'd expect older references to exist, but I have not managed to find any…

**Tags:** reference-request, lambda-calculus
> **Comments:**
> **username_1**: Papers about the "lambda calculus with constructors" might be relevant. And you can also try using a keyword that relates to the possibility of error states (since you now have functions and pairs, but no types to prevent cross interactions), e.g. "error", "clash", or "daimon".  
> **username_1**: Papers that cite "The virtues of eta-expansion" might also be relevant  

---

## 0 answers

