5
$\begingroup$

Let $M, N, P, Q$ be pure untyped lambda terms.

Suppose that $M \stackrel{*}\rightarrow P, Q$ and $N \stackrel{*}\rightarrow P, Q,$ where $\stackrel{*}\rightarrow$ denotes that the term on the left can be reduced to the term on the right by applying $\beta$-reduction zero or more times.

Does there always exist a lambda term $R$ such that $M, N \stackrel{*}\rightarrow R$ and $R \stackrel{*}\rightarrow P, Q$?

My assumption is that if two lambda terms are $\beta$-equivalent, then the reduction diagram of the two lambda terms should meet at a unique point:

the diagram

$\endgroup$
3
  • $\begingroup$ Welcome to MSE. Your question is phrased as an isolated problem, without any further information or context. This does not match many users' quality standards, so it may attract downvotes, or be closed. To prevent that, please edit the question. This will help you recognize and resolve the issues. Concretely: please provide context, and include your work and thoughts on the problem. These changes can help in formulating more appropriate answers. $\endgroup$ Commented Nov 8 at 10:56
  • 1
    $\begingroup$ It's not quite clear to me what context is missing. The phrasing is minimalist but clearly states a problem, only relying on unambiguous basic material. $\endgroup$ Commented Nov 8 at 15:19
  • 1
    $\begingroup$ Just so I know (as the question was closed in the end), @JoséCarlosSantos, what kind of context should have been added? I suspect people want 'untyped lambda term' to be defined, which is a bit ridiculous. One wouldn't ask for the definition of 'measure' or 'functor'. (Is math.meta.SE intended for such a question? genuinely asking.) $\endgroup$ Commented Nov 14 at 12:02

1 Answer 1

Reset to default
6
$\begingroup$

No.

Define the usual Church encoding of booleans, $T := λxy.x$ and $F := λxy.y$. Then we can define: $$M := T(Fyx)y \qquad N := Fy(Txy)$$ so that $M \to^* Txy$ (by evaluating the inner boolean) and $M \to^* Fyx$ (by evaluating the outer one), and similarly $N \to^* Fyx$ and $N \to^* Txy$. (Notice that by confluence of β-reduction I had to choose $P$ and $Q$ with a common reduct, namely $x$.)

Observe that all reduction $M \to R$ destroys either the subterm $T$ or the subterm $F$, hence either $R \to^* Txy$ or $R \to^* Fyx$ becomes impossible. The same holds for $N$. As a consequence, $M$ and $N$ share no common reduct $R$ with the desired property.

$\endgroup$
2
  • 1
    $\begingroup$ Nice example! As a picture, this is a sort of atomic "bowtie" ($\bowtie$) with no intermediate step. $\endgroup$ Commented Nov 8 at 18:32
  • $\begingroup$ Thanks :-) My first version was in fact $T(Fyx)(Fxy)$ and $F(Tyx)(Txy)$, which you would call non-atomic (?), and could be simplified. $\endgroup$ Commented Nov 8 at 22:50

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.