All Questions
18
questions
2
votes
1
answer
29
views
$(\lambda z. zy)(\lambda z. zy)$ - reducing using $\beta$ reduction and $\alpha$ conversion
Good day . I need to reduce the following expression of lambda calculus:
$(\lambda z. zy)(\lambda z. zy)$
Now, since I am having the variable $y$ in both the left and right pair of parentheses, I ...
- 893
1
vote
1
answer
112
views
Why is a head redex always the leftmost redex?
I am studying lambda-calculus from Sorensen's book (Lectures on the Curry-Howard Isomorphism, 2006 edition), and on page 15 there is a definition of 'head redex'
in a lambda term $\lambda\vec{z}.(\...
4
votes
1
answer
102
views
Lambda calculus novice seeking help with defining isempty for list representation
I'm exploring the concept of untyped lambda calculus and I'm facing a challenge with defining the isempty function. I have a few definitions that I'm working with, which are:
...
- 41
1
vote
1
answer
193
views
Lambda Calculus: Proving exponent property by induction
Recently I have learned that given Church numerals $\bar n = \lambda fx.f^n x$ and $\bar m = \lambda fx.f^m x$, we can calculate $\overline{m^n}$ by applying $\exp=\lambda mn.nm$. I believe this means ...
- 23
2
votes
1
answer
84
views
A confusion on $\beta\eta$-reduction
Recently I've started exploring lambda calculus, and currently I'm tackling the next exercise:
Prove that if $M =_{\beta\eta} N$, then $FV(M) = FV(N)$,
Where $FV(P)$ stands for free variables in the ...
- 432
2
votes
1
answer
726
views
Lambda Calculus Xor
How do you prove $\mathsf{xor} \, \mathsf{True}\, \mathsf{True}$ is false in lambda calculus using call-by-value reduction.
This is the approach I tried but it is not working:
$$\mathsf{xor} \equiv \...
1
vote
0
answers
50
views
Lambda Calculus Beta Reduction - How do I do this?
I'm trying to figure out a Lambda Calculus 𝛽-reduction, but I can't seem to get my head around whether I'm doing this correctly.
Beta reduction problem
I'm trying to beta reduce ...
- 11
3
votes
1
answer
244
views
Proving terms using induction in LC
Expanding on the following question here and on the book on the $\lambda$-calculus I'm reading, I'm trying to prove the correctness of the given solution in a more complicated manner.
Let $(F_n')_{n \...
- 125
2
votes
1
answer
870
views
Lambda calculus - church encoding and lists
I'm reading a book on the $\lambda$-calculus and I'm stuck on a list of representations. While practising different lambda calculus tasks I've stumbled upon an interesting issue. Given two terms I ...
- 125
1
vote
1
answer
181
views
Beta reducing $SS(SK)$ using SKI calculus
I have an expression to $\beta$-reduce and I managed to brute force it using the $\lambda$-calculus. I was wondering though, if I could make it in less steps, than what I did, using the $SKI$-calculus....
- 515
3
votes
1
answer
84
views
Why is reflexivity a feature of multi-step β-reduction, and not of β-reduction?
I understand the need to distinguish between two algorithms, even when one is enclosed in another. Transitivity as a feature of multi-step reduction makes perfect sense, since we literally need ...
- 692
3
votes
1
answer
52
views
Lambda Calculus Question: If for some λ-terms M and N we have Mx =β Nx. Does it necessarily imply that M =β N?
I have a homework question that I can't figure out. Hope someone can help.
Assume that for some $\lambda$-terms $M$ and $N$ we have $Mx =_\beta Nx$. Does it necessarily imply that $M =_\beta N$?
Here ...
- 33
2
votes
1
answer
187
views
Parenthesization in Lambda Calculus
I am trying to understand how parenthesization works in $λ$-calculus. All of the resources state the following:
Applications are left associative;
Abstractions are right associative and extend as ...
- 339
3
votes
1
answer
377
views
Representation of Church numerals
In the $\lambda$-calculus, is the family of $\lambda$-terms $(N_i)_{i \in \mathbb{N}}$, defined below, a representation of Church numerals? I think it is, but how do I (sufficiently) show it? If not, ...
user156182
-1
votes
1
answer
1k
views
Lambda Calculus Beta reductions
I have two questions about $\beta$-reduction in the $\lambda$-calculus. Please find them below. I have also included some background information about how lists (i.e. finite sequences) can be encoded ...
user867914