0
$\begingroup$

I tried to complete this exercise but i stopped... Defining a $ \lambda $-term M such that: $$(<M,u>)<M,v> \: \simeq_{\beta} \: <M,u>$$

I chose $M=\lambda m \lambda a \lambda b \lambda p \,((p)m)b \:$ then i have to find a representation T of a function using M that value true if the sequence is empty and false if it's not. A sequence is defined as: $$[]=\lambda x_0\lambda x_1 \lambda z z \\ [b]=\lambda x_0 \lambda x_1 \lambda z (z) x_b\\ [b_1 b_2]=\lambda x_0 \lambda x_1 \lambda z ((z)x_{b_1})x_{b_2} \\ .\\. \\ . \\ [b_1 .. b_n]= \lambda x_0 \lambda x_1 \lambda z (...((z) x_{b_1})x_{b_2}...)x_{b_n} $$ so the sequence of exercise is : $$[01101]= \lambda x_0 \lambda x_1 \lambda z (((((z)x_0)x_1)x_1)x_0)x_1 $$ For example T need to be: $(T)[01101] \simeq_{\beta}$ false while $ (T) []\simeq_{\beta}$ true. I really find that difficult. How i can do that?

edit.

$true=λxλyx$ and $false=λxλyy$

Improve this question
$\endgroup$
3
  • $\begingroup$ What are true and false terms in your lambda calculus? $\endgroup$ Commented Jan 29, 2020 at 23:27
  • $\begingroup$ $true = \lambda x \lambda y x $ and $false = \lambda x \lambda y y$ i'm sorry I forget to write them in the post $\endgroup$ Commented Jan 30, 2020 at 0:17
  • $\begingroup$ that’s what edit is for, no worries! $\endgroup$ Commented Jan 30, 2020 at 0:23

1 Answer 1

Reset to default
1
$\begingroup$

We can remove the dependence on what the values stored in the sequences are by assuming that we pass "the same thing" as the first two arguments. Regardless of what $b_1, b_2, b_3$ are:

$$([b_1b_2b_3]\,x)\,x = \lambda f. ((f\,x)\,x)\,x$$

This gives you an effective way to tell the difference between an empty sequence and a non-empty sequence :

$$(([]\left<M,u\right>)\left<M,u\right>)\,(\lambda x. x) = \lambda x. x$$ $$(([b_1]\left<M,u\right>)\left<M,u\right>)\,(\lambda x. x) = \left<M,u\right>$$ $$(([b_1b_2]\left<M,u\right>)\left<M,u\right>)\,(\lambda x. x) = \left<M,u\right>$$ $$(([b_1b_2b_3]\left<M,u\right>)\left<M,u\right>)\,(\lambda x. x) = \left<M,u\right>$$

So if $s$ is a sequence, consider this:

$$((((s\left<M,u\right>) \left<M,u\right>) (\lambda x. x))\,\hbox{false}$$

What does it reduce to if $s$ is empty? What does it reduce to if it's non-empty?

Improve this answer
$\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.