2

$ \newcommand{\abstraction}[2]{\lambda #1. #2}$ $\newcommand{\application}[2]{\left(#1 #2\right)}$ $\newcommand{\substitution}[3]{#1 \left[#2 := #3\right]}$ $ \newcommand{\freevars}[1]{\operatorname{FV}\left(#1\right)}$ $\newcommand{\closedlambdaset}{\Lambda^{0}}$ $\newcommand{\lambdaexprswithfreevars}[1]{\closedlambdaset\left(#1\right)}$ $\newcommand{\subterm}[1]{\operatorname{Sub}\left(#1\right)}$ $\newcommand{\vars}[1]{\operatorname{Var}\left(#1\right)}$ $\newcommand{\context}[2]{{#1}\left[#2\right]}$ $\newcommand{\hole}{\ }$

I am trying to prove the following statement in Lambda calculus: \begin{equation} \forall \context{C}{\hole} \in \Lambda, \forall \vec{x}, \exists F \in \Lambda, \forall M \in \lambdaexprswithfreevars{\vec{x}}, \context{C}{M} = \application{F}{\left(\abstraction{\vec{x}}{M}\right)}, \end{equation} where $\context{C}{\hole}$ is a context, and $\lambdaexprswithfreevars{\vec{x}}$ is the set of all $\lambda$-expression with free variables covered by $\vec{x}$:

\begin{equation} \lambdaexprswithfreevars{\vec{x}} = \left\{ M \in \Lambda \vert \freevars{M} \subseteq \left\{\vec{x}\right\} \right\}. \end{equation}

I understand that we need to use induction to prove this lemma. However, I got stuck on the simplest case. For instance, first assume that $\context{C}{\hole} \equiv y$, a free variable, and $\vec{x}$ is an arbitrary vector of variables. Under this assumption, $\context{C}{M} = y$. Then we need to find an $F$ such that $\application{F}{\left(\abstraction{\vec{x}}{M}\right)} = y$. How should I construct such an $F$?

Next assume that $\context{C}{\hole} \equiv \context{}{\hole}$. Under this assumption, $\context{C}{M} = M$. Again, we need to construct an $F$ such that $M = \application{F}{\left(\abstraction{\vec{x}}{M}\right)}$. How should I construct this $F$?

I am attaching the definition of contexts here in case is it unclear: $x$ is a context; $\left[\ \right]$ is a context; if $\context{C_{1}}{\ }$ and $\context{C_{2}}{\ }$ are both contexts, so are $\application{\context{C_{1}}{\ }}{\context{C_{2}}{\ }}$ and $\abstraction{x}{\context{C_{1}}{\ }}$. Actually, I am curious why a single variable is thought of as a context. The original definition can be found on page 29 of "the lambda calculus: its syntax and semantics".

Ziqi Fan
  • 1,816
  • 1
    I've edited your question to format the MathJax. Firstly, please make sure my edit reflects the way you intended your question to look like. Secondly, take the time to edit the contents of your question further. As it is now, it is quite probable to be poorly received by the community. Try adding more context and also show your work or thoughts on the problem. – Stefan Octavian Dec 24 '21 at 21:13
  • Yes, thanks. I made the post for a trial. Sometimes, I found that preview didn't render all math expressions in latex. They are only updated in the real post. – Ziqi Fan Dec 24 '21 at 21:15
  • Great, you have already added your work/thoughts on the matter by the time I wrote the previous comment. Looks like some context might still be necessary, but perhaps it's just my limited knowledge of lambda-calcalus – Stefan Octavian Dec 24 '21 at 21:16
  • What is your exact definition contexts $C[]$? Are you sure they can be a variable? – frabala Dec 24 '21 at 21:54
  • @frabala In page 29 of "the lambda calculus: its syntax and semantics", there is a formal definition for contexts. The first statement is that $x$ is a context. Please feel free to correct me if I had a misunderstanding. – Ziqi Fan Dec 24 '21 at 22:44

2 Answers2

2

I don't remember ever seeing a definition of a context to include a variable. A plain variable does not have a hole, after all. But, moving on...

$F$ does not need to be well-scoped. So, for the base case where $C=y$, you can define $F$ to be $\lambda f.y$.

For the next base case, where $C[\,]=[\,]$, you can define $F$ to be the function $\lambda f. f\,\vec{x}$, where $\vec{x}$ is the $\vec{x}$ given by the statement. Then $C[M] = M$ and $F\,(\lambda\vec{x}.M) = (\lambda f. f\,\vec{x})\,(\lambda\vec{x}.M)$.

Note that in both cases, the two terms are not syntactically equal, but they are $\beta$-equivalent.

frabala
  • 3,732
  • In the inductive case, $F(\lambda\vec{x}.M) = (\lambda f. f \vec{x})(\lambda \vec{x}.M)$ which further β-reduces to normal form $\lambda \vec{x}.M \vec{x}$, so it seems it's βη-equivalent to $C[M]=M$, not simply β-equivalent. Any clarification? – cinch Dec 27 '21 at 06:53
  • I think you've got the reduction wrong. It goes like this: $$(\lambda f. f,\vec{x}),(\lambda\vec{y}.M) ~\to_\beta~ (\lambda\vec{y}.M),\vec{x}~\to_\beta~ M[\vec{x}/\vec{y}]$$ and the two terms are $\beta\eta$-equivlent.

    I've renamed the bound variables to $\vec{y}$, to make things more clear.

     – frabala Dec 27 '21 at 11:18
0

$\newcommand{\abstraction}[2]{\lambda #1. #2}$ $\newcommand{\application}[2]{\left(#1 #2\right)}$ $\newcommand{\substitution}[3]{#1 \left[#2 := #3\right]}$ $\newcommand{\freevars}[1]{\operatorname{FV}\left(#1\right)}$ $\newcommand{\closedlambdaset}{\Lambda^{0}}$ $\newcommand{\lambdaexprswithfreevars}[1]{\closedlambdaset\left(#1\right)}$ $\newcommand{\subterm}[1]{\operatorname{Sub}\left(#1\right)}$ $\newcommand{\vars}[1]{\operatorname{Var}\left(#1\right)}$ $\newcommand{\context}[2]{{#1}\left[#2\right]}$ $\newcommand{\hole}{\ }$

I've been trying to prove the same theorem for a few days now: lemma 2.1.20(i) of Barendregt's The Lambda Calculus, Its Syntax and Semantics. The answer by fragala in this thread helped me advance as I was stuck trying to define a single $F$ for all 4 cases. So I went like so:

I want $F\left(\abstraction{\vec{x}}{M}\right) = C[M]$.

Abstracting $M$ on the rhs: $F \left(\abstraction{\vec{x}}{M}\right) = \left(\abstraction{g}{\context{C}{\application {g}{\vec{x}}}}\right) \left(\abstraction{\vec{x}}{M}\right)$ Resulting in the choice of $F = \abstraction{g}{\context{C}{\application {g}{\vec{x}}}}$

By induction on the structure of the context.

  • Case 1: $\context{C}{} = a$ and $\context{C}{M} = a$.

    Then $F = \abstraction{g}{a}$ and $F \left(\abstraction{\vec{x}}{M}\right) = \left( \abstraction{g}{a} \right) \left(\abstraction{\vec{x}}{M}\right) = a = \context{C}{M}$

  • Case 2. $\context{C}{} = \context{}{}$ and $\context{C}{M} = M$.

    Then $F = \abstraction{g}{\application{g}{\vec{x}}}$ and $F \left(\abstraction{\vec{x}}{M}\right) = \left( \abstraction{g}{\application{g}{\vec{x}}} \right) \left(\abstraction{\vec{x}}{M}\right) = \left(\abstraction{\vec{x}}{M}\right) \vec{x} = M = \context{C}{M}$

Note that the above are equivalent to frabala's.

  • Case 3. $\context{C}{} = \abstraction{y}{\context{C_1}{}}$ and $\context{c}{M} = \abstraction{y}{\context{C_1}{M}}$ such that $\context{C_1}{M} = F \left( \abstraction{\vec{x}}{M} \right)$ as per the induction hypothesis.

    Then $F \left( \abstraction{\vec{x}}{M} \right) = \left( \abstraction{g}{\abstraction{y}{\context{C_1}{\application{g}{\vec{x}}}}} \right) \left( \abstraction{\vec{x}}{M} \right) = \abstraction{y}{\context{C_1}{\left( \abstraction{\vec{x}}{M} \right) \vec{x}}} = \abstraction{y}{\context{C_1}{M}} = \context{C}{M}$

  • Case 4. $\context{C}{} = \application{\context{C_1}{}}{\context{C_2}{}}$ and $\context{C}{M} = \application{\context{C_1}{M}}{\context{C_2}{M}}$ such that $\context{C_1}{M} = F_1 \left( \abstraction{\vec{x}}{M} \right)$ and $\context{C_2}{M} = F_2 \left( \abstraction{\vec{x}}{M} \right)$ per the induction hypothesis.

    Then $F \left( \abstraction{\vec{x}}{M} \right) = \left(\abstraction{g}{\application{\context{C_1}{\application{g}{\vec{x}}}}{\context{C_2}{\application{g}{\vec{x}}}}}\right)\left( \abstraction{\vec{x}}{M} \right) = \application{\context{C_1}{M}}{\context{C_2}{M}} = \context{C}{M}$

What annoys me is that I didn't need the induction hypothesis in cases 3 and 4.

Edil
  • 21