4
$\begingroup$

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?

$\endgroup$
8
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.