Ambiguity of definition of substitution in lambda calculus
$begingroup$
From Type Theory and Formal Proof, An Introduction by Rob Nederpelt and Herman Geuvers:
Definition 1.6.1 (Substitution)
(1a) $x[x := N] equiv N$,
(1b) $y[x := N] equiv y$ if $x not equiv y$,
(2) $(PQ)[x := N] equiv (P[x := N])(Q[x := N])$,
(3) $(lambda y . P)[x := N] equiv lambda z . (P^{y to z} [x := N])$, if $lambda z . P^{y to z}$ is an $alpha$-variant of $lambda y . P$ such that $z notin FV(N)$.
If I look at $(lambda y . y)[y := a]$ then it seems that I can have either:
$(lambda y . y)[y := a] = lambda y . (y[y := a]) = lambda y . a$
or
$(lambda y . y)[y := a] = lambda z . (z[y := a]) = lambda z . z$
These are very different. Have I missed something in the definition?
lambda-calculus
asked Dec 19 '18 at 23:09
user695931user695931
17511
$endgroup$
add a comment |
$begingroup$
From Type Theory and Formal Proof, An Introduction by Rob Nederpelt and Herman Geuvers:
Definition 1.6.1 (Substitution)
(1a) $x[x := N] equiv N$,
(1b) $y[x := N] equiv y$ if $x not equiv y$,
(2) $(PQ)[x := N] equiv (P[x := N])(Q[x := N])$,
(3) $(lambda y . P)[x := N] equiv lambda z . (P^{y to z} [x := N])$, if $lambda z . P^{y to z}$ is an $alpha$-variant of $lambda y . P$ such that $z notin FV(N)$.
If I look at $(lambda y . y)[y := a]$ then it seems that I can have either:
$(lambda y . y)[y := a] = lambda y . (y[y := a]) = lambda y . a$
or
$(lambda y . y)[y := a] = lambda z . (z[y := a]) = lambda z . z$
These are very different. Have I missed something in the definition?
lambda-calculus
asked Dec 19 '18 at 23:09
user695931user695931
17511
$endgroup$
$begingroup$
Maybe (3) is missing the condition that you should have $z notequiv x$ which would invalidate the first substitution? (Not sure, not being completely familiar with the notation being used here - but the first result is definitely the suspect one.)
$endgroup$
– Daniel Schepler
Dec 19 '18 at 23:20
$begingroup$
The wikipedia definition seems to differ from this one: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 0:49
add a comment |
$begingroup$
From Type Theory and Formal Proof, An Introduction by Rob Nederpelt and Herman Geuvers:
Definition 1.6.1 (Substitution)
(1a) $x[x := N] equiv N$,
(1b) $y[x := N] equiv y$ if $x not equiv y$,
(2) $(PQ)[x := N] equiv (P[x := N])(Q[x := N])$,
(3) $(lambda y . P)[x := N] equiv lambda z . (P^{y to z} [x := N])$, if $lambda z . P^{y to z}$ is an $alpha$-variant of $lambda y . P$ such that $z notin FV(N)$.
If I look at $(lambda y . y)[y := a]$ then it seems that I can have either:
$(lambda y . y)[y := a] = lambda y . (y[y := a]) = lambda y . a$
or
$(lambda y . y)[y := a] = lambda z . (z[y := a]) = lambda z . z$
These are very different. Have I missed something in the definition?
lambda-calculus
asked Dec 19 '18 at 23:09
user695931user695931
17511
$endgroup$
From Type Theory and Formal Proof, An Introduction by Rob Nederpelt and Herman Geuvers:
Definition 1.6.1 (Substitution)
(1a) $x[x := N] equiv N$,
(1b) $y[x := N] equiv y$ if $x not equiv y$,
(2) $(PQ)[x := N] equiv (P[x := N])(Q[x := N])$,
(3) $(lambda y . P)[x := N] equiv lambda z . (P^{y to z} [x := N])$, if $lambda z . P^{y to z}$ is an $alpha$-variant of $lambda y . P$ such that $z notin FV(N)$.
If I look at $(lambda y . y)[y := a]$ then it seems that I can have either:
$(lambda y . y)[y := a] = lambda y . (y[y := a]) = lambda y . a$
or
$(lambda y . y)[y := a] = lambda z . (z[y := a]) = lambda z . z$
These are very different. Have I missed something in the definition?
lambda-calculus
lambda-calculus
asked Dec 19 '18 at 23:09
user695931user695931
17511
asked Dec 19 '18 at 23:09
user695931user695931
17511
asked Dec 19 '18 at 23:09
user695931user695931
17511
asked Dec 19 '18 at 23:09
user695931user695931
17511
asked Dec 19 '18 at 23:09
user695931user695931
17511
17511
$begingroup$
Maybe (3) is missing the condition that you should have $z notequiv x$ which would invalidate the first substitution? (Not sure, not being completely familiar with the notation being used here - but the first result is definitely the suspect one.)
$endgroup$
– Daniel Schepler
Dec 19 '18 at 23:20
$begingroup$
The wikipedia definition seems to differ from this one: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 0:49
add a comment |
$begingroup$
Maybe (3) is missing the condition that you should have $z notequiv x$ which would invalidate the first substitution? (Not sure, not being completely familiar with the notation being used here - but the first result is definitely the suspect one.)
$endgroup$
– Daniel Schepler
Dec 19 '18 at 23:20
$begingroup$
The wikipedia definition seems to differ from this one: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 0:49
$begingroup$
Maybe (3) is missing the condition that you should have $z notequiv x$ which would invalidate the first substitution? (Not sure, not being completely familiar with the notation being used here - but the first result is definitely the suspect one.)
$endgroup$
– Daniel Schepler
Dec 19 '18 at 23:20
$begingroup$
Maybe (3) is missing the condition that you should have $z notequiv x$ which would invalidate the first substitution? (Not sure, not being completely familiar with the notation being used here - but the first result is definitely the suspect one.)
$endgroup$
– Daniel Schepler
Dec 19 '18 at 23:20
$begingroup$
The wikipedia definition seems to differ from this one: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 0:49
$begingroup$
The wikipedia definition seems to differ from this one: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 0:49
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Clearly, $lambda y. a$ and $lambda z.z$ are different (in the sense of not $alpha$-equivalent) terms.
Actually, $(lambda y. y)[y := a] = lambda z. z = lambda y. y,$ (up to $alpha$-equivalence) and there is no ambiguity.
Indeed, according to definition 1.6.1 in Nederpelt' and Geuvers' handbook, $(lambda y.y)[y:=a] neq lambda y.(y[y:=a])$ because in general $lambda z . P^{y to z}$ is defined provided that $z notin FV(P)$ (see definition 1.5.1) and this condition does not hold in $lambda y.y$ (where $z = y = P$).
answered Dec 19 '18 at 23:28
TaroccoesbroccoTaroccoesbrocco
5,56271840
$endgroup$
$begingroup$
I thought it would hold by remark 1.6.3 (1)?
$endgroup$
– user695931
Dec 20 '18 at 1:05
1
$begingroup$
@user695931 - In Remark 1.6.3 (1) it is implicitly assumed that $x neq y$. Remind the intuitive meaning of substitution (explained just before definition 1.6.1): $M[x := N]$ stands for $M$ in which $N$ has been substituted for the free variable $x$. Clearly, in $M = lambda y. P$ the variable $y$ is bound, so if $x = y$ then $(lambda y.P)[x := N]) = lambda y.P$ (no substitution is performed): this is exactly what happens for $(lambda y.y)[y:=a]$.
$endgroup$
– Taroccoesbrocco
Dec 20 '18 at 9:04
$begingroup$
I guess this makes sense. It seems confusing that they made the condition $x not equiv y$ explicit in 1b, but not here. The wikipedia version seems a bit clearer: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 15:32
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%2f3046968%2fambiguity-of-definition-of-substitution-in-lambda-calculus%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$
Clearly, $lambda y. a$ and $lambda z.z$ are different (in the sense of not $alpha$-equivalent) terms.
Actually, $(lambda y. y)[y := a] = lambda z. z = lambda y. y,$ (up to $alpha$-equivalence) and there is no ambiguity.
Indeed, according to definition 1.6.1 in Nederpelt' and Geuvers' handbook, $(lambda y.y)[y:=a] neq lambda y.(y[y:=a])$ because in general $lambda z . P^{y to z}$ is defined provided that $z notin FV(P)$ (see definition 1.5.1) and this condition does not hold in $lambda y.y$ (where $z = y = P$).
answered Dec 19 '18 at 23:28
TaroccoesbroccoTaroccoesbrocco
5,56271840
$endgroup$
$begingroup$
I thought it would hold by remark 1.6.3 (1)?
$endgroup$
– user695931
Dec 20 '18 at 1:05
1
$begingroup$
@user695931 - In Remark 1.6.3 (1) it is implicitly assumed that $x neq y$. Remind the intuitive meaning of substitution (explained just before definition 1.6.1): $M[x := N]$ stands for $M$ in which $N$ has been substituted for the free variable $x$. Clearly, in $M = lambda y. P$ the variable $y$ is bound, so if $x = y$ then $(lambda y.P)[x := N]) = lambda y.P$ (no substitution is performed): this is exactly what happens for $(lambda y.y)[y:=a]$.
$endgroup$
– Taroccoesbrocco
Dec 20 '18 at 9:04
$begingroup$
I guess this makes sense. It seems confusing that they made the condition $x not equiv y$ explicit in 1b, but not here. The wikipedia version seems a bit clearer: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 15:32
add a comment |
$begingroup$
Clearly, $lambda y. a$ and $lambda z.z$ are different (in the sense of not $alpha$-equivalent) terms.
Actually, $(lambda y. y)[y := a] = lambda z. z = lambda y. y,$ (up to $alpha$-equivalence) and there is no ambiguity.
Indeed, according to definition 1.6.1 in Nederpelt' and Geuvers' handbook, $(lambda y.y)[y:=a] neq lambda y.(y[y:=a])$ because in general $lambda z . P^{y to z}$ is defined provided that $z notin FV(P)$ (see definition 1.5.1) and this condition does not hold in $lambda y.y$ (where $z = y = P$).
answered Dec 19 '18 at 23:28
TaroccoesbroccoTaroccoesbrocco
5,56271840
$endgroup$
$begingroup$
I thought it would hold by remark 1.6.3 (1)?
$endgroup$
– user695931
Dec 20 '18 at 1:05
1
$begingroup$
@user695931 - In Remark 1.6.3 (1) it is implicitly assumed that $x neq y$. Remind the intuitive meaning of substitution (explained just before definition 1.6.1): $M[x := N]$ stands for $M$ in which $N$ has been substituted for the free variable $x$. Clearly, in $M = lambda y. P$ the variable $y$ is bound, so if $x = y$ then $(lambda y.P)[x := N]) = lambda y.P$ (no substitution is performed): this is exactly what happens for $(lambda y.y)[y:=a]$.
$endgroup$
– Taroccoesbrocco
Dec 20 '18 at 9:04
$begingroup$
I guess this makes sense. It seems confusing that they made the condition $x not equiv y$ explicit in 1b, but not here. The wikipedia version seems a bit clearer: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 15:32
add a comment |
$begingroup$
Clearly, $lambda y. a$ and $lambda z.z$ are different (in the sense of not $alpha$-equivalent) terms.
Actually, $(lambda y. y)[y := a] = lambda z. z = lambda y. y,$ (up to $alpha$-equivalence) and there is no ambiguity.
Indeed, according to definition 1.6.1 in Nederpelt' and Geuvers' handbook, $(lambda y.y)[y:=a] neq lambda y.(y[y:=a])$ because in general $lambda z . P^{y to z}$ is defined provided that $z notin FV(P)$ (see definition 1.5.1) and this condition does not hold in $lambda y.y$ (where $z = y = P$).
answered Dec 19 '18 at 23:28
TaroccoesbroccoTaroccoesbrocco
5,56271840
$endgroup$
Clearly, $lambda y. a$ and $lambda z.z$ are different (in the sense of not $alpha$-equivalent) terms.
Actually, $(lambda y. y)[y := a] = lambda z. z = lambda y. y,$ (up to $alpha$-equivalence) and there is no ambiguity.
Indeed, according to definition 1.6.1 in Nederpelt' and Geuvers' handbook, $(lambda y.y)[y:=a] neq lambda y.(y[y:=a])$ because in general $lambda z . P^{y to z}$ is defined provided that $z notin FV(P)$ (see definition 1.5.1) and this condition does not hold in $lambda y.y$ (where $z = y = P$).
answered Dec 19 '18 at 23:28
TaroccoesbroccoTaroccoesbrocco
5,56271840
answered Dec 19 '18 at 23:28
TaroccoesbroccoTaroccoesbrocco
5,56271840
answered Dec 19 '18 at 23:28
TaroccoesbroccoTaroccoesbrocco
5,56271840
answered Dec 19 '18 at 23:28
TaroccoesbroccoTaroccoesbrocco
5,56271840
5,56271840
$begingroup$
I thought it would hold by remark 1.6.3 (1)?
$endgroup$
– user695931
Dec 20 '18 at 1:05
1
$begingroup$
@user695931 - In Remark 1.6.3 (1) it is implicitly assumed that $x neq y$. Remind the intuitive meaning of substitution (explained just before definition 1.6.1): $M[x := N]$ stands for $M$ in which $N$ has been substituted for the free variable $x$. Clearly, in $M = lambda y. P$ the variable $y$ is bound, so if $x = y$ then $(lambda y.P)[x := N]) = lambda y.P$ (no substitution is performed): this is exactly what happens for $(lambda y.y)[y:=a]$.
$endgroup$
– Taroccoesbrocco
Dec 20 '18 at 9:04
$begingroup$
I guess this makes sense. It seems confusing that they made the condition $x not equiv y$ explicit in 1b, but not here. The wikipedia version seems a bit clearer: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 15:32
add a comment |
$begingroup$
I thought it would hold by remark 1.6.3 (1)?
$endgroup$
– user695931
Dec 20 '18 at 1:05
1
$begingroup$
@user695931 - In Remark 1.6.3 (1) it is implicitly assumed that $x neq y$. Remind the intuitive meaning of substitution (explained just before definition 1.6.1): $M[x := N]$ stands for $M$ in which $N$ has been substituted for the free variable $x$. Clearly, in $M = lambda y. P$ the variable $y$ is bound, so if $x = y$ then $(lambda y.P)[x := N]) = lambda y.P$ (no substitution is performed): this is exactly what happens for $(lambda y.y)[y:=a]$.
$endgroup$
– Taroccoesbrocco
Dec 20 '18 at 9:04
$begingroup$
I guess this makes sense. It seems confusing that they made the condition $x not equiv y$ explicit in 1b, but not here. The wikipedia version seems a bit clearer: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 15:32
$begingroup$
I thought it would hold by remark 1.6.3 (1)?
$endgroup$
– user695931
Dec 20 '18 at 1:05
$begingroup$
I thought it would hold by remark 1.6.3 (1)?
$endgroup$
– user695931
Dec 20 '18 at 1:05
1
1
$begingroup$
@user695931 - In Remark 1.6.3 (1) it is implicitly assumed that $x neq y$. Remind the intuitive meaning of substitution (explained just before definition 1.6.1): $M[x := N]$ stands for $M$ in which $N$ has been substituted for the free variable $x$. Clearly, in $M = lambda y. P$ the variable $y$ is bound, so if $x = y$ then $(lambda y.P)[x := N]) = lambda y.P$ (no substitution is performed): this is exactly what happens for $(lambda y.y)[y:=a]$.
$endgroup$
– Taroccoesbrocco
Dec 20 '18 at 9:04
$begingroup$
@user695931 - In Remark 1.6.3 (1) it is implicitly assumed that $x neq y$. Remind the intuitive meaning of substitution (explained just before definition 1.6.1): $M[x := N]$ stands for $M$ in which $N$ has been substituted for the free variable $x$. Clearly, in $M = lambda y. P$ the variable $y$ is bound, so if $x = y$ then $(lambda y.P)[x := N]) = lambda y.P$ (no substitution is performed): this is exactly what happens for $(lambda y.y)[y:=a]$.
$endgroup$
– Taroccoesbrocco
Dec 20 '18 at 9:04
$begingroup$
I guess this makes sense. It seems confusing that they made the condition $x not equiv y$ explicit in 1b, but not here. The wikipedia version seems a bit clearer: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 15:32
$begingroup$
I guess this makes sense. It seems confusing that they made the condition $x not equiv y$ explicit in 1b, but not here. The wikipedia version seems a bit clearer: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 15:32
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%2f3046968%2fambiguity-of-definition-of-substitution-in-lambda-calculus%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$
Maybe (3) is missing the condition that you should have $z notequiv x$ which would invalidate the first substitution? (Not sure, not being completely familiar with the notation being used here - but the first result is definitely the suspect one.)
$endgroup$
– Daniel Schepler
Dec 19 '18 at 23:20
$begingroup$
The wikipedia definition seems to differ from this one: en.wikipedia.org/wiki/Lambda_calculus#Substitution
$endgroup$
– user695931
Dec 20 '18 at 0:49