Mixing
lambda calculus evaluation
$begingroup$
I have a question about lambda calculus. I just read that it doesn't matter in which way expressions get evaluated.
So my question is: $(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
so we can evaluate this expression like this:
$(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
$(lambda x.(λy.y+1)(lambda y.y+1)x) 2$
$((lambda y.y+1)(lambda y.y+1)2)$
$(lambda y.y+1)(2+1)$
$2+1+1$
but what if we start evaluation like this:
$(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
$(lambda f.lambda x.f(fx)) (2+1)$ ???
So how can I continue evaluation now? I know there should be some rules not letting me to start evaluation like this but what is that?
computer-science lambda-calculus
edited Jan 9 at 14:07
Taroccoesbrocco
5,26571839
asked Jan 9 at 13:02
Amin Nasim saraviAmin Nasim saravi
62
$endgroup$
add a comment |
$begingroup$
I have a question about lambda calculus. I just read that it doesn't matter in which way expressions get evaluated.
So my question is: $(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
so we can evaluate this expression like this:
$(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
$(lambda x.(λy.y+1)(lambda y.y+1)x) 2$
$((lambda y.y+1)(lambda y.y+1)2)$
$(lambda y.y+1)(2+1)$
$2+1+1$
but what if we start evaluation like this:
$(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
$(lambda f.lambda x.f(fx)) (2+1)$ ???
So how can I continue evaluation now? I know there should be some rules not letting me to start evaluation like this but what is that?
computer-science lambda-calculus
edited Jan 9 at 14:07
Taroccoesbrocco
5,26571839
asked Jan 9 at 13:02
Amin Nasim saraviAmin Nasim saravi
62
$endgroup$
$begingroup$
hey Amin, please use LaTeX or MathJax to edit your question.. Your question is not readable, thereby decreasing the probability of help. An example of a readable equation could be $$x^2 + 2x + 1 = f(x) $$
$endgroup$
– Ahmad Bazzi
Jan 9 at 13:03
add a comment |
$begingroup$
I have a question about lambda calculus. I just read that it doesn't matter in which way expressions get evaluated.
So my question is: $(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
so we can evaluate this expression like this:
$(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
$(lambda x.(λy.y+1)(lambda y.y+1)x) 2$
$((lambda y.y+1)(lambda y.y+1)2)$
$(lambda y.y+1)(2+1)$
$2+1+1$
but what if we start evaluation like this:
$(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
$(lambda f.lambda x.f(fx)) (2+1)$ ???
So how can I continue evaluation now? I know there should be some rules not letting me to start evaluation like this but what is that?
computer-science lambda-calculus
edited Jan 9 at 14:07
Taroccoesbrocco
5,26571839
asked Jan 9 at 13:02
Amin Nasim saraviAmin Nasim saravi
62
$endgroup$
I have a question about lambda calculus. I just read that it doesn't matter in which way expressions get evaluated.
So my question is: $(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
so we can evaluate this expression like this:
$(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
$(lambda x.(λy.y+1)(lambda y.y+1)x) 2$
$((lambda y.y+1)(lambda y.y+1)2)$
$(lambda y.y+1)(2+1)$
$2+1+1$
but what if we start evaluation like this:
$(lambda f.lambda x.f(fx)) (lambda y.y+1) 2$
$(lambda f.lambda x.f(fx)) (2+1)$ ???
So how can I continue evaluation now? I know there should be some rules not letting me to start evaluation like this but what is that?
computer-science lambda-calculus
computer-science lambda-calculus
edited Jan 9 at 14:07
Taroccoesbrocco
5,26571839
asked Jan 9 at 13:02
Amin Nasim saraviAmin Nasim saravi
62
edited Jan 9 at 14:07
Taroccoesbrocco
5,26571839
asked Jan 9 at 13:02
Amin Nasim saraviAmin Nasim saravi
62
edited Jan 9 at 14:07
Taroccoesbrocco
5,26571839
edited Jan 9 at 14:07
Taroccoesbrocco
5,26571839
edited Jan 9 at 14:07
Taroccoesbrocco
5,26571839
5,26571839
asked Jan 9 at 13:02
Amin Nasim saraviAmin Nasim saravi
62
asked Jan 9 at 13:02
Amin Nasim saraviAmin Nasim saravi
62
asked Jan 9 at 13:02
Amin Nasim saraviAmin Nasim saravi
62
62
$begingroup$
hey Amin, please use LaTeX or MathJax to edit your question.. Your question is not readable, thereby decreasing the probability of help. An example of a readable equation could be $$x^2 + 2x + 1 = f(x) $$
$endgroup$
– Ahmad Bazzi
Jan 9 at 13:03
add a comment |
$begingroup$
hey Amin, please use LaTeX or MathJax to edit your question.. Your question is not readable, thereby decreasing the probability of help. An example of a readable equation could be $$x^2 + 2x + 1 = f(x) $$
$endgroup$
– Ahmad Bazzi
Jan 9 at 13:03
$begingroup$
hey Amin, please use LaTeX or MathJax to edit your question.. Your question is not readable, thereby decreasing the probability of help. An example of a readable equation could be $$x^2 + 2x + 1 = f(x) $$
$endgroup$
– Ahmad Bazzi
Jan 9 at 13:03
$begingroup$
hey Amin, please use LaTeX or MathJax to edit your question.. Your question is not readable, thereby decreasing the probability of help. An example of a readable equation could be $$x^2 + 2x + 1 = f(x) $$
$endgroup$
– Ahmad Bazzi
Jan 9 at 13:03
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
It is true that in the $lambda$-calculus it doesn't matter in which way expressions get evaluated, provided that the evaluation ends in a normal form (i.e. in a term that cannot be reduced any further). This property is called uniqueness of the normal form and it is a consequence of confluence.
Your term does not contradict the uniqueness of the normal form. Indeed, in $(lambda f. lambda x.f(fx)) (lambda y.y+1) 2$ there is only one $beta$-redex, i.e. only one sub-term that can be reduced: $(lambda f. lambda x.f(fx)) (lambda y.y+1)$. Thus, you can start only the first evaluation you wrote.
Why? If you have a term of the form $MNL$ then it has to be read as $(MN)L$, and you cannot read it as $M(NL)$. This is the unambiguous way terms are defined in the $lambda$-calculus.
So, your term $(lambda f. lambda x.f(fx)) (lambda y.y+1) 2$ is actually $big( (lambda f. lambda x.f(fx)) (lambda y.y+1) big) 2$ and hence you cannot start the second evaluation you wrote.
Note that there is the same mistake also at the end of your first evaluation: the term $(lambda y.y+1)(lambda y.y+1)2$ has to be read as $big( (lambda y.y+1)(lambda y.y+1) big) 2$ and not as $(lambda y.y+1) big((lambda y.y+1)2big)$, hence it $beta$-reduces to $(lambda y.y+1+1) 2$ and not to $(lambda y.y+1) (2+1)$.
answered Jan 9 at 14:03
TaroccoesbroccoTaroccoesbrocco
5,26571839
$endgroup$
1
$begingroup$
The order of evaluation does affect whether you reach a normal form or not. Two different evaluation order can't lead to two different normal forms, but one can fail to reach a normal form while the other succeeds.
$endgroup$
– Derek Elkins
Jan 21 at 19:49
$begingroup$
@DerekElkins - You are right, thank you for the specification. I edited my answer. Anyway, note that by confluence whatever term $t$ is reached according to any evaluation starting from a term $t_0$, the unique normal form of $t_0$ can always be reached from $t$.
$endgroup$
– Taroccoesbrocco
Jan 21 at 20:00
$begingroup$
What is the reason of the downvote?
$endgroup$
– Taroccoesbrocco
Jan 22 at 3:21
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3067425%2flambda-calculus-evaluation%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
It is true that in the $lambda$-calculus it doesn't matter in which way expressions get evaluated, provided that the evaluation ends in a normal form (i.e. in a term that cannot be reduced any further). This property is called uniqueness of the normal form and it is a consequence of confluence.
Your term does not contradict the uniqueness of the normal form. Indeed, in $(lambda f. lambda x.f(fx)) (lambda y.y+1) 2$ there is only one $beta$-redex, i.e. only one sub-term that can be reduced: $(lambda f. lambda x.f(fx)) (lambda y.y+1)$. Thus, you can start only the first evaluation you wrote.
Why? If you have a term of the form $MNL$ then it has to be read as $(MN)L$, and you cannot read it as $M(NL)$. This is the unambiguous way terms are defined in the $lambda$-calculus.
So, your term $(lambda f. lambda x.f(fx)) (lambda y.y+1) 2$ is actually $big( (lambda f. lambda x.f(fx)) (lambda y.y+1) big) 2$ and hence you cannot start the second evaluation you wrote.
Note that there is the same mistake also at the end of your first evaluation: the term $(lambda y.y+1)(lambda y.y+1)2$ has to be read as $big( (lambda y.y+1)(lambda y.y+1) big) 2$ and not as $(lambda y.y+1) big((lambda y.y+1)2big)$, hence it $beta$-reduces to $(lambda y.y+1+1) 2$ and not to $(lambda y.y+1) (2+1)$.
answered Jan 9 at 14:03
TaroccoesbroccoTaroccoesbrocco
5,26571839
$endgroup$
1
$begingroup$
The order of evaluation does affect whether you reach a normal form or not. Two different evaluation order can't lead to two different normal forms, but one can fail to reach a normal form while the other succeeds.
$endgroup$
– Derek Elkins
Jan 21 at 19:49
$begingroup$
@DerekElkins - You are right, thank you for the specification. I edited my answer. Anyway, note that by confluence whatever term $t$ is reached according to any evaluation starting from a term $t_0$, the unique normal form of $t_0$ can always be reached from $t$.
$endgroup$
– Taroccoesbrocco
Jan 21 at 20:00
$begingroup$
What is the reason of the downvote?
$endgroup$
– Taroccoesbrocco
Jan 22 at 3:21
add a comment |
$begingroup$
It is true that in the $lambda$-calculus it doesn't matter in which way expressions get evaluated, provided that the evaluation ends in a normal form (i.e. in a term that cannot be reduced any further). This property is called uniqueness of the normal form and it is a consequence of confluence.
Your term does not contradict the uniqueness of the normal form. Indeed, in $(lambda f. lambda x.f(fx)) (lambda y.y+1) 2$ there is only one $beta$-redex, i.e. only one sub-term that can be reduced: $(lambda f. lambda x.f(fx)) (lambda y.y+1)$. Thus, you can start only the first evaluation you wrote.
Why? If you have a term of the form $MNL$ then it has to be read as $(MN)L$, and you cannot read it as $M(NL)$. This is the unambiguous way terms are defined in the $lambda$-calculus.
So, your term $(lambda f. lambda x.f(fx)) (lambda y.y+1) 2$ is actually $big( (lambda f. lambda x.f(fx)) (lambda y.y+1) big) 2$ and hence you cannot start the second evaluation you wrote.
Note that there is the same mistake also at the end of your first evaluation: the term $(lambda y.y+1)(lambda y.y+1)2$ has to be read as $big( (lambda y.y+1)(lambda y.y+1) big) 2$ and not as $(lambda y.y+1) big((lambda y.y+1)2big)$, hence it $beta$-reduces to $(lambda y.y+1+1) 2$ and not to $(lambda y.y+1) (2+1)$.
answered Jan 9 at 14:03
TaroccoesbroccoTaroccoesbrocco
5,26571839
$endgroup$
1
$begingroup$
The order of evaluation does affect whether you reach a normal form or not. Two different evaluation order can't lead to two different normal forms, but one can fail to reach a normal form while the other succeeds.
$endgroup$
– Derek Elkins
Jan 21 at 19:49
$begingroup$
@DerekElkins - You are right, thank you for the specification. I edited my answer. Anyway, note that by confluence whatever term $t$ is reached according to any evaluation starting from a term $t_0$, the unique normal form of $t_0$ can always be reached from $t$.
$endgroup$
– Taroccoesbrocco
Jan 21 at 20:00
$begingroup$
What is the reason of the downvote?
$endgroup$
– Taroccoesbrocco
Jan 22 at 3:21
add a comment |
$begingroup$
It is true that in the $lambda$-calculus it doesn't matter in which way expressions get evaluated, provided that the evaluation ends in a normal form (i.e. in a term that cannot be reduced any further). This property is called uniqueness of the normal form and it is a consequence of confluence.
Your term does not contradict the uniqueness of the normal form. Indeed, in $(lambda f. lambda x.f(fx)) (lambda y.y+1) 2$ there is only one $beta$-redex, i.e. only one sub-term that can be reduced: $(lambda f. lambda x.f(fx)) (lambda y.y+1)$. Thus, you can start only the first evaluation you wrote.
Why? If you have a term of the form $MNL$ then it has to be read as $(MN)L$, and you cannot read it as $M(NL)$. This is the unambiguous way terms are defined in the $lambda$-calculus.
So, your term $(lambda f. lambda x.f(fx)) (lambda y.y+1) 2$ is actually $big( (lambda f. lambda x.f(fx)) (lambda y.y+1) big) 2$ and hence you cannot start the second evaluation you wrote.
Note that there is the same mistake also at the end of your first evaluation: the term $(lambda y.y+1)(lambda y.y+1)2$ has to be read as $big( (lambda y.y+1)(lambda y.y+1) big) 2$ and not as $(lambda y.y+1) big((lambda y.y+1)2big)$, hence it $beta$-reduces to $(lambda y.y+1+1) 2$ and not to $(lambda y.y+1) (2+1)$.
answered Jan 9 at 14:03
TaroccoesbroccoTaroccoesbrocco
5,26571839
$endgroup$
It is true that in the $lambda$-calculus it doesn't matter in which way expressions get evaluated, provided that the evaluation ends in a normal form (i.e. in a term that cannot be reduced any further). This property is called uniqueness of the normal form and it is a consequence of confluence.
Your term does not contradict the uniqueness of the normal form. Indeed, in $(lambda f. lambda x.f(fx)) (lambda y.y+1) 2$ there is only one $beta$-redex, i.e. only one sub-term that can be reduced: $(lambda f. lambda x.f(fx)) (lambda y.y+1)$. Thus, you can start only the first evaluation you wrote.
Why? If you have a term of the form $MNL$ then it has to be read as $(MN)L$, and you cannot read it as $M(NL)$. This is the unambiguous way terms are defined in the $lambda$-calculus.
So, your term $(lambda f. lambda x.f(fx)) (lambda y.y+1) 2$ is actually $big( (lambda f. lambda x.f(fx)) (lambda y.y+1) big) 2$ and hence you cannot start the second evaluation you wrote.
Note that there is the same mistake also at the end of your first evaluation: the term $(lambda y.y+1)(lambda y.y+1)2$ has to be read as $big( (lambda y.y+1)(lambda y.y+1) big) 2$ and not as $(lambda y.y+1) big((lambda y.y+1)2big)$, hence it $beta$-reduces to $(lambda y.y+1+1) 2$ and not to $(lambda y.y+1) (2+1)$.
answered Jan 9 at 14:03
TaroccoesbroccoTaroccoesbrocco
5,26571839
edited Jan 21 at 19:57
answered Jan 9 at 14:03
TaroccoesbroccoTaroccoesbrocco
5,26571839
answered Jan 9 at 14:03
TaroccoesbroccoTaroccoesbrocco
5,26571839
answered Jan 9 at 14:03
TaroccoesbroccoTaroccoesbrocco
5,26571839
5,26571839
1
$begingroup$
The order of evaluation does affect whether you reach a normal form or not. Two different evaluation order can't lead to two different normal forms, but one can fail to reach a normal form while the other succeeds.
$endgroup$
– Derek Elkins
Jan 21 at 19:49
$begingroup$
@DerekElkins - You are right, thank you for the specification. I edited my answer. Anyway, note that by confluence whatever term $t$ is reached according to any evaluation starting from a term $t_0$, the unique normal form of $t_0$ can always be reached from $t$.
$endgroup$
– Taroccoesbrocco
Jan 21 at 20:00
$begingroup$
What is the reason of the downvote?
$endgroup$
– Taroccoesbrocco
Jan 22 at 3:21
add a comment |
1
$begingroup$
The order of evaluation does affect whether you reach a normal form or not. Two different evaluation order can't lead to two different normal forms, but one can fail to reach a normal form while the other succeeds.
$endgroup$
– Derek Elkins
Jan 21 at 19:49
$begingroup$
@DerekElkins - You are right, thank you for the specification. I edited my answer. Anyway, note that by confluence whatever term $t$ is reached according to any evaluation starting from a term $t_0$, the unique normal form of $t_0$ can always be reached from $t$.
$endgroup$
– Taroccoesbrocco
Jan 21 at 20:00
$begingroup$
What is the reason of the downvote?
$endgroup$
– Taroccoesbrocco
Jan 22 at 3:21
1
1
$begingroup$
The order of evaluation does affect whether you reach a normal form or not. Two different evaluation order can't lead to two different normal forms, but one can fail to reach a normal form while the other succeeds.
$endgroup$
– Derek Elkins
Jan 21 at 19:49
$begingroup$
The order of evaluation does affect whether you reach a normal form or not. Two different evaluation order can't lead to two different normal forms, but one can fail to reach a normal form while the other succeeds.
$endgroup$
– Derek Elkins
Jan 21 at 19:49
$begingroup$
@DerekElkins - You are right, thank you for the specification. I edited my answer. Anyway, note that by confluence whatever term $t$ is reached according to any evaluation starting from a term $t_0$, the unique normal form of $t_0$ can always be reached from $t$.
$endgroup$
– Taroccoesbrocco
Jan 21 at 20:00
$begingroup$
@DerekElkins - You are right, thank you for the specification. I edited my answer. Anyway, note that by confluence whatever term $t$ is reached according to any evaluation starting from a term $t_0$, the unique normal form of $t_0$ can always be reached from $t$.
$endgroup$
– Taroccoesbrocco
Jan 21 at 20:00
$begingroup$
What is the reason of the downvote?
$endgroup$
– Taroccoesbrocco
Jan 22 at 3:21
$begingroup$
What is the reason of the downvote?
$endgroup$
– Taroccoesbrocco
Jan 22 at 3:21
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3067425%2flambda-calculus-evaluation%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
$begingroup$
hey Amin, please use LaTeX or MathJax to edit your question.. Your question is not readable, thereby decreasing the probability of help. An example of a readable equation could be $$x^2 + 2x + 1 = f(x) $$
$endgroup$
– Ahmad Bazzi
Jan 9 at 13:03