<p>You might want to look at Barry Jay's Pattern Calculus. This is something beyond the $\lambda$-calculus, but is has the power to do intensional analysis of lambda expressions.</p>

CC BY-SA 3.0
2013-06-07T11:14:09.903Z
2013-06-07T11:14:09.903Z
Dave Clarke
<p>The Böhm-out technique can construct term contexts that can distinguish between terms iff they are distinct in the beta-eta theory (i.e., a term context $C[-]$ so that $C[s]=T$ and $C[t]=F$). See, e.g., <a href="http://www.di.unito.it/~dezani/papers/dgp.pdf">http://www.di.unito.it/~dezani/papers/dgp.pdf</a> - it is exceedingly systemtic.</p>

<p>If the terms are closed, as in your example, the context you construct using the Böhm-out technique will be a term M that you apply to the two terms (so $M s = T$, $M t=F$).  Otherwise the term context will include capturing substitutions so that it can work at the sites of the free variables.</p>

CC BY-SA 3.0
2013-06-07T12:02:12.760Z
2013-06-07T12:07:38.563Z
2013-06-07T12:07:38.563Z
Charles Stewart
<p>For example, finding terms $\vec{a}$ such that:</p>

<p>$\vec{a}(\lambda x.x) = T\\\vec{a}(\lambda xy.x) = F$</p>

<p>Is there a systematic method for finding terms with these types of constraint?</p>

<lambda-calculus>
Is there a systematic method for constructing lambda calculus terms that can distinguish between inputs?
tjs
# Is there a systematic method for constructing lambda calculus terms that can distinguish between inputs?

(Asked by: username_0 on 2013-06-07)

For example, finding terms $\vec{a}$ such that:

$\vec{a}(\lambda x.x) = T\\\vec{a}(\lambda xy.x) = F$

Is there a systematic method for finding terms with these types of constraint?

**Tags:** lambda-calculus

---

## 2 answers

### Answer by username_2 on 2013-06-07. Score: 7 | Accepted answer

The Böhm-out technique can construct term contexts that can distinguish between terms iff they are distinct in the beta-eta theory (i.e., a term context $C[-]$ so that $C[s]=T$ and $C[t]=F$). See, e.g., <http://www.di.unito.it/~dezani/papers/dgp.pdf> - it is exceedingly systemtic.

If the terms are closed, as in your example, the context you construct using the Böhm-out technique will be a term M that you apply to the two terms (so $M s = T$, $M t=F$). Otherwise the term context will include capturing substitutions so that it can work at the sites of the free variables.


---

### Answer by username_1 on 2013-06-07. Score: 0

You might want to look at Barry Jay's Pattern Calculus. This is something beyond the $\lambda$-calculus, but is has the power to do intensional analysis of lambda expressions.


---

