0
$\begingroup$

I am working through a textbook on type theory and I came across a proof of a statement on $\beta-$equality that I don't understand. It states as follows: $$(\lambda y. yv)z =_{\beta} (\lambda x. zx)v$$ To prove this the following chain is provided: $$(\lambda y. yv)z \rightarrow_{\beta} zv \leftarrow_{\beta} (\lambda x. zx)v$$

I do not understand what "$\leftarrow_{\beta}$" means. The book states that it is the inverse of "$\rightarrow_{\beta}$".

How does $\textit{undoing}$ a $\beta-$reduction result in a simpler term i.e. $zv$?

$\endgroup$
2
  • 3
    $\begingroup$ Please clarify your question. $\leftarrow_\beta$ is indeed defined as the inverse of $\to_\beta$, i.e. $u \leftarrow_\beta t$ iff $t \to_\beta u$. It does not result in a "simpler" term, whatever this means, in general (nor a more complicated term). It is just doing a $\beta$-reduction backwards (a $\beta$-expansion, if you like). $\endgroup$ Commented Jul 6 at 16:03
  • $\begingroup$ it's just meant to be read right to left. $(λy.yv)z$ β-reduces to zv and so does $(λx.zx)v$ $\endgroup$ Commented Aug 19 at 20:31

1 Answer 1

Reset to default
0
$\begingroup$

$\beta$-reduction $\to_\beta$ is a binary relation on the set $\Lambda$ of $\lambda$-terms. More precisely, $\to_\beta$ is the smallest subset of $\Lambda \times \Lambda$ such that (using the infix the notation):

  • $(\lambda x.M)N \to_\beta M\{N/x\}$
  • $M \to_\beta N \implies \lambda x.M \to_\beta \lambda x.N$
  • $M \to_\beta N \implies LM \to_\beta LN$
  • $M \to_\beta N \implies ML \to_\beta NL$

$\beta$-expansion ${}_\beta\!\!\leftarrow$ is nothing but the converse relation (aka inverse relation or transpose) of $\to_\beta$, that is, $${}_\beta\!\!\leftarrow \ = \ \{(M,N) \in \Lambda \times \Lambda \mid N \to_\beta M\} $$ in other words: $M {}_\beta\!\!\leftarrow N \iff N \to_\beta M$. Intuitively, $\beta$-expansion performs a $\beta$-reduction step backwards. In your case, as $(\lambda x.zx)v \to_\beta zv$, then $zv \, {}_\beta\!\!\leftarrow (\lambda x.zx)v$. Note that the same $\lambda$-term can be obtained by performing $\beta$-reduction from two different $\lambda$-terms, such as $zv$ that can be obtained from $(\lambda y.yv)z \to_\beta zv$ and $(\lambda x.zx)v \to_\beta zv$.

The idea that $\beta$-reduction or $\beta$-expansion "simplifies" a term is quite misleading, unless you define precisely what "simpler" means. Roughly, you can see $\beta$-reduction as a computation step that brings you "closer" to the output of the computation (a $\lambda$-term where there are no more $\beta$-redexes to fire). In this respect, $\beta$-expansion moves you a step "farther" than the output. According to this computational point of view, $\beta$-equivalence $=_\beta$ (that is, the reflexive-transitive closure of $\to_\beta \cup \, {}_\beta\!\!\leftarrow$) just represents two different stages of two computations leading to the same output.

$\endgroup$

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.