Recursive Definition of Normal Form with explicit substitutionLambda Calculus: beta-reduction and predecessor functionLambda Calculus: Reducing to Normal FormPure Lambda Calculus: Call-by-value Free Variable Argument Application ReductionProving that $Omega = (lambda x.xx)(lambda x.xx)$ is not typable in the simply typed lambda calculusAre untyped and simply typed lambda calculus mutually exclusive?$beta$ inequality in $lambda$-calculusAre common lambda calculus notation conventions sloppy?Formal rules for the summation convention? (Lambda Calculus $alpha$-equivalence?)Can a lambda term with only a free variable be reduced furtherLambda calculus, $M$ doesn't have a normal form, $N$ has normal form. Find $M N$ that has a normal form?
Should I install hardwood flooring or cabinets first?
Did US corporations pay demonstrators in the German demonstrations against article 13?
How much character growth crosses the line into breaking the character
Can I Retrieve Email Addresses from BCC?
Bob has never been a M before
Do the concepts of IP address and network interface not belong to the same layer?
List of people who lose a child in תנ"ך
Drawing a topological "handle" with Tikz
A Permanent Norse Presence in America
Why is Arduino resetting while driving motors?
Greco-Roman egalitarianism
Drawing ramified coverings with tikz
Indicating multiple different modes of speech (fantasy language or telepathy)
Engineer refusing to file/disclose patents
Why does the integral domain "being trapped between a finite field extension" implies that it is a field?
Proving a function is onto where f(x)=|x|.
Diode in opposite direction?
Did arcade monitors have same pixel aspect ratio as TV sets?
Does having a TSA Pre-Check member in your flight reservation increase the chances that everyone gets Pre-Check?
On a tidally locked planet, would time be quantized?
Java - What do constructor type arguments mean when placed *before* the type?
Have I saved too much for retirement so far?
Is there a conventional notation or name for the slip angle?
Why has "pence" been used in this sentence, not "pences"?
Recursive Definition of Normal Form with explicit substitution
Lambda Calculus: beta-reduction and predecessor functionLambda Calculus: Reducing to Normal FormPure Lambda Calculus: Call-by-value Free Variable Argument Application ReductionProving that $Omega = (lambda x.xx)(lambda x.xx)$ is not typable in the simply typed lambda calculusAre untyped and simply typed lambda calculus mutually exclusive?$beta$ inequality in $lambda$-calculusAre common lambda calculus notation conventions sloppy?Formal rules for the summation convention? (Lambda Calculus $alpha$-equivalence?)Can a lambda term with only a free variable be reduced furtherLambda calculus, $M$ doesn't have a normal form, $N$ has normal form. Find $M N$ that has a normal form?
$begingroup$
Context
I assume a simply typed lambda calculus, probably written with de-bruijn indexes. With $to_beta$ I denote the $beta$-reduction as a relation.
Also, my question eventually will use this $lambda$-calculus with explicit substitution (originally called $lambdasigma$-calculus), where substitution is introduced on term level via closures $M[s]$ with $lambda$-term M and substitution $s$.
A few definitions are needed.
Definition: Normal Form
A $lambda$-term $M$ is in normal form, if there is no $lambda$-term $N$ such that $Mto_beta N$.
Besides this defintion, there is also another definition I'm ultimately interested in: defining normal form recursively:
Definition II: Neutral and Normal Form
Mutually defining neutral and normal forms:
Neutral Form:
- Every variable is in neutral form.
- if $M$ is in neutral form and $N$ in normal form then $(M N)$ is in neutral form.
Normal Form:
- If $M$ is in neutral form, then $M$ is in normal form.
- If $M$ is in normal form, then $lambda M$ is in normal form.
Question
So far, this deals with the classical simply typed lambda calculus, where substitution is defined as a (meta-) function over terms.
First: does this definition of normal forms make sense?
Then: Putting substitution into the term level, the question arises how to define normal forms then recursively as above?
Own Ideas
My first go to was to add the following case to the definition of a normal form:
- If every term in $s$ is in neutral form and $t$ is in normal form, then $t[s]$ is in normal form.
Since neutral forms don't allow abstractions, even when dealing with closures like $(x y)[s]$, this should not introduce new $beta$-redexes. But somehow, I'm unsure. Does this still resemble what NF means? After searching for information, there seems to be nothing like this.
substitution lambda-calculus
asked Mar 16 at 11:17
aphorismeaphorisme
61438
$endgroup$
|
show 2 more comments
$begingroup$
Context
I assume a simply typed lambda calculus, probably written with de-bruijn indexes. With $to_beta$ I denote the $beta$-reduction as a relation.
Also, my question eventually will use this $lambda$-calculus with explicit substitution (originally called $lambdasigma$-calculus), where substitution is introduced on term level via closures $M[s]$ with $lambda$-term M and substitution $s$.
A few definitions are needed.
Definition: Normal Form
A $lambda$-term $M$ is in normal form, if there is no $lambda$-term $N$ such that $Mto_beta N$.
Besides this defintion, there is also another definition I'm ultimately interested in: defining normal form recursively:
Definition II: Neutral and Normal Form
Mutually defining neutral and normal forms:
Neutral Form:
- Every variable is in neutral form.
- if $M$ is in neutral form and $N$ in normal form then $(M N)$ is in neutral form.
Normal Form:
- If $M$ is in neutral form, then $M$ is in normal form.
- If $M$ is in normal form, then $lambda M$ is in normal form.
Question
So far, this deals with the classical simply typed lambda calculus, where substitution is defined as a (meta-) function over terms.
First: does this definition of normal forms make sense?
Then: Putting substitution into the term level, the question arises how to define normal forms then recursively as above?
Own Ideas
My first go to was to add the following case to the definition of a normal form:
- If every term in $s$ is in neutral form and $t$ is in normal form, then $t[s]$ is in normal form.
Since neutral forms don't allow abstractions, even when dealing with closures like $(x y)[s]$, this should not introduce new $beta$-redexes. But somehow, I'm unsure. Does this still resemble what NF means? After searching for information, there seems to be nothing like this.
substitution lambda-calculus
asked Mar 16 at 11:17
aphorismeaphorisme
61438
$endgroup$
$begingroup$
Why require the terms in $s$ to be neutral? This does not allow explicit substitutions with lambdas.
$endgroup$
– frabala
Mar 16 at 14:53
$begingroup$
Well, if they are normal, then consider $s = [x leftarrow lambda M, yleftarrow N]$ where $M,N$ are normal, so every term in $s$ is normal. But then $(x y)[s]$ contains a redex. Substitution by itself is allowed to contain lambdas, but when preserving normal forms, this is not allowed.
$endgroup$
– aphorisme
Mar 16 at 14:56
$begingroup$
I don't see a redex in $(x, y)[xleftarrowlambda M, yleftarrow N]$. Aren't redexes directly applied lambdas on an argument? Do you perhaps consider another reduction rule that would justify $(x, y)[xleftarrow t_1, yleftarrow t_2]$ reducing to $(t_1 y)[yleftarrow t_2]$?
$endgroup$
– frabala
Mar 16 at 15:04
$begingroup$
Hm, maybe I've assumed things I should have mentioned. Besides adding substitution on term level, there are a few equations added as well. Especially terms $M[s]$ and $N$ are equal, if $N$ is $M$ where $M$ is substituted according to $s$ ... so in my example $(x y)[s]$ becomes $((lambda M)N)$. Okay, I see, there are a few subtelties, I cannot see since I'm too deep in.
$endgroup$
– aphorisme
Mar 16 at 15:07
$begingroup$
You want to maintain an equivalence that a value is in normal form if and only if it is irreducible. However, you add a new reduction rule for terms of the form $t[s]$. Then, if you want the equivalence preserved, in definition II terms of the form $t[s]$ should not be in normal nor neutral form. So, definition II stays as is.
$endgroup$
– frabala
Mar 16 at 15:56
|
show 2 more comments
$begingroup$
Context
I assume a simply typed lambda calculus, probably written with de-bruijn indexes. With $to_beta$ I denote the $beta$-reduction as a relation.
Also, my question eventually will use this $lambda$-calculus with explicit substitution (originally called $lambdasigma$-calculus), where substitution is introduced on term level via closures $M[s]$ with $lambda$-term M and substitution $s$.
A few definitions are needed.
Definition: Normal Form
A $lambda$-term $M$ is in normal form, if there is no $lambda$-term $N$ such that $Mto_beta N$.
Besides this defintion, there is also another definition I'm ultimately interested in: defining normal form recursively:
Definition II: Neutral and Normal Form
Mutually defining neutral and normal forms:
Neutral Form:
- Every variable is in neutral form.
- if $M$ is in neutral form and $N$ in normal form then $(M N)$ is in neutral form.
Normal Form:
- If $M$ is in neutral form, then $M$ is in normal form.
- If $M$ is in normal form, then $lambda M$ is in normal form.
Question
So far, this deals with the classical simply typed lambda calculus, where substitution is defined as a (meta-) function over terms.
First: does this definition of normal forms make sense?
Then: Putting substitution into the term level, the question arises how to define normal forms then recursively as above?
Own Ideas
My first go to was to add the following case to the definition of a normal form:
- If every term in $s$ is in neutral form and $t$ is in normal form, then $t[s]$ is in normal form.
Since neutral forms don't allow abstractions, even when dealing with closures like $(x y)[s]$, this should not introduce new $beta$-redexes. But somehow, I'm unsure. Does this still resemble what NF means? After searching for information, there seems to be nothing like this.
substitution lambda-calculus
asked Mar 16 at 11:17
aphorismeaphorisme
61438
$endgroup$
Context
I assume a simply typed lambda calculus, probably written with de-bruijn indexes. With $to_beta$ I denote the $beta$-reduction as a relation.
Also, my question eventually will use this $lambda$-calculus with explicit substitution (originally called $lambdasigma$-calculus), where substitution is introduced on term level via closures $M[s]$ with $lambda$-term M and substitution $s$.
A few definitions are needed.
Definition: Normal Form
A $lambda$-term $M$ is in normal form, if there is no $lambda$-term $N$ such that $Mto_beta N$.
Besides this defintion, there is also another definition I'm ultimately interested in: defining normal form recursively:
Definition II: Neutral and Normal Form
Mutually defining neutral and normal forms:
Neutral Form:
- Every variable is in neutral form.
- if $M$ is in neutral form and $N$ in normal form then $(M N)$ is in neutral form.
Normal Form:
- If $M$ is in neutral form, then $M$ is in normal form.
- If $M$ is in normal form, then $lambda M$ is in normal form.
Question
So far, this deals with the classical simply typed lambda calculus, where substitution is defined as a (meta-) function over terms.
First: does this definition of normal forms make sense?
Then: Putting substitution into the term level, the question arises how to define normal forms then recursively as above?
Own Ideas
My first go to was to add the following case to the definition of a normal form:
- If every term in $s$ is in neutral form and $t$ is in normal form, then $t[s]$ is in normal form.
Since neutral forms don't allow abstractions, even when dealing with closures like $(x y)[s]$, this should not introduce new $beta$-redexes. But somehow, I'm unsure. Does this still resemble what NF means? After searching for information, there seems to be nothing like this.
substitution lambda-calculus
substitution lambda-calculus
asked Mar 16 at 11:17
aphorismeaphorisme
61438
asked Mar 16 at 11:17
aphorismeaphorisme
61438
asked Mar 16 at 11:17
aphorismeaphorisme
61438
asked Mar 16 at 11:17
aphorismeaphorisme
61438
asked Mar 16 at 11:17
aphorismeaphorisme
61438
61438
$begingroup$
Why require the terms in $s$ to be neutral? This does not allow explicit substitutions with lambdas.
$endgroup$
– frabala
Mar 16 at 14:53
$begingroup$
Well, if they are normal, then consider $s = [x leftarrow lambda M, yleftarrow N]$ where $M,N$ are normal, so every term in $s$ is normal. But then $(x y)[s]$ contains a redex. Substitution by itself is allowed to contain lambdas, but when preserving normal forms, this is not allowed.
$endgroup$
– aphorisme
Mar 16 at 14:56
$begingroup$
I don't see a redex in $(x, y)[xleftarrowlambda M, yleftarrow N]$. Aren't redexes directly applied lambdas on an argument? Do you perhaps consider another reduction rule that would justify $(x, y)[xleftarrow t_1, yleftarrow t_2]$ reducing to $(t_1 y)[yleftarrow t_2]$?
$endgroup$
– frabala
Mar 16 at 15:04
$begingroup$
Hm, maybe I've assumed things I should have mentioned. Besides adding substitution on term level, there are a few equations added as well. Especially terms $M[s]$ and $N$ are equal, if $N$ is $M$ where $M$ is substituted according to $s$ ... so in my example $(x y)[s]$ becomes $((lambda M)N)$. Okay, I see, there are a few subtelties, I cannot see since I'm too deep in.
$endgroup$
– aphorisme
Mar 16 at 15:07
$begingroup$
You want to maintain an equivalence that a value is in normal form if and only if it is irreducible. However, you add a new reduction rule for terms of the form $t[s]$. Then, if you want the equivalence preserved, in definition II terms of the form $t[s]$ should not be in normal nor neutral form. So, definition II stays as is.
$endgroup$
– frabala
Mar 16 at 15:56
|
show 2 more comments
$begingroup$
Why require the terms in $s$ to be neutral? This does not allow explicit substitutions with lambdas.
$endgroup$
– frabala
Mar 16 at 14:53
$begingroup$
Well, if they are normal, then consider $s = [x leftarrow lambda M, yleftarrow N]$ where $M,N$ are normal, so every term in $s$ is normal. But then $(x y)[s]$ contains a redex. Substitution by itself is allowed to contain lambdas, but when preserving normal forms, this is not allowed.
$endgroup$
– aphorisme
Mar 16 at 14:56
$begingroup$
I don't see a redex in $(x, y)[xleftarrowlambda M, yleftarrow N]$. Aren't redexes directly applied lambdas on an argument? Do you perhaps consider another reduction rule that would justify $(x, y)[xleftarrow t_1, yleftarrow t_2]$ reducing to $(t_1 y)[yleftarrow t_2]$?
$endgroup$
– frabala
Mar 16 at 15:04
$begingroup$
Hm, maybe I've assumed things I should have mentioned. Besides adding substitution on term level, there are a few equations added as well. Especially terms $M[s]$ and $N$ are equal, if $N$ is $M$ where $M$ is substituted according to $s$ ... so in my example $(x y)[s]$ becomes $((lambda M)N)$. Okay, I see, there are a few subtelties, I cannot see since I'm too deep in.
$endgroup$
– aphorisme
Mar 16 at 15:07
$begingroup$
You want to maintain an equivalence that a value is in normal form if and only if it is irreducible. However, you add a new reduction rule for terms of the form $t[s]$. Then, if you want the equivalence preserved, in definition II terms of the form $t[s]$ should not be in normal nor neutral form. So, definition II stays as is.
$endgroup$
– frabala
Mar 16 at 15:56
$begingroup$
Why require the terms in $s$ to be neutral? This does not allow explicit substitutions with lambdas.
$endgroup$
– frabala
Mar 16 at 14:53
$begingroup$
Why require the terms in $s$ to be neutral? This does not allow explicit substitutions with lambdas.
$endgroup$
– frabala
Mar 16 at 14:53
$begingroup$
Well, if they are normal, then consider $s = [x leftarrow lambda M, yleftarrow N]$ where $M,N$ are normal, so every term in $s$ is normal. But then $(x y)[s]$ contains a redex. Substitution by itself is allowed to contain lambdas, but when preserving normal forms, this is not allowed.
$endgroup$
– aphorisme
Mar 16 at 14:56
$begingroup$
Well, if they are normal, then consider $s = [x leftarrow lambda M, yleftarrow N]$ where $M,N$ are normal, so every term in $s$ is normal. But then $(x y)[s]$ contains a redex. Substitution by itself is allowed to contain lambdas, but when preserving normal forms, this is not allowed.
$endgroup$
– aphorisme
Mar 16 at 14:56
$begingroup$
I don't see a redex in $(x, y)[xleftarrowlambda M, yleftarrow N]$. Aren't redexes directly applied lambdas on an argument? Do you perhaps consider another reduction rule that would justify $(x, y)[xleftarrow t_1, yleftarrow t_2]$ reducing to $(t_1 y)[yleftarrow t_2]$?
$endgroup$
– frabala
Mar 16 at 15:04
$begingroup$
I don't see a redex in $(x, y)[xleftarrowlambda M, yleftarrow N]$. Aren't redexes directly applied lambdas on an argument? Do you perhaps consider another reduction rule that would justify $(x, y)[xleftarrow t_1, yleftarrow t_2]$ reducing to $(t_1 y)[yleftarrow t_2]$?
$endgroup$
– frabala
Mar 16 at 15:04
$begingroup$
Hm, maybe I've assumed things I should have mentioned. Besides adding substitution on term level, there are a few equations added as well. Especially terms $M[s]$ and $N$ are equal, if $N$ is $M$ where $M$ is substituted according to $s$ ... so in my example $(x y)[s]$ becomes $((lambda M)N)$. Okay, I see, there are a few subtelties, I cannot see since I'm too deep in.
$endgroup$
– aphorisme
Mar 16 at 15:07
$begingroup$
Hm, maybe I've assumed things I should have mentioned. Besides adding substitution on term level, there are a few equations added as well. Especially terms $M[s]$ and $N$ are equal, if $N$ is $M$ where $M$ is substituted according to $s$ ... so in my example $(x y)[s]$ becomes $((lambda M)N)$. Okay, I see, there are a few subtelties, I cannot see since I'm too deep in.
$endgroup$
– aphorisme
Mar 16 at 15:07
$begingroup$
You want to maintain an equivalence that a value is in normal form if and only if it is irreducible. However, you add a new reduction rule for terms of the form $t[s]$. Then, if you want the equivalence preserved, in definition II terms of the form $t[s]$ should not be in normal nor neutral form. So, definition II stays as is.
$endgroup$
– frabala
Mar 16 at 15:56
$begingroup$
You want to maintain an equivalence that a value is in normal form if and only if it is irreducible. However, you add a new reduction rule for terms of the form $t[s]$. Then, if you want the equivalence preserved, in definition II terms of the form $t[s]$ should not be in normal nor neutral form. So, definition II stays as is.
$endgroup$
– frabala
Mar 16 at 15:56
|
show 2 more comments
1 Answer
1
active
oldest
votes
$begingroup$
Does the recursive definition make sense?
I'm guessing, this question in more formal terms would be "Are the two definitions equivalent?". To answer this, you can try to show that for every term $t$,
- if it has no more redexes, it is in II-normal form (short for "normal form by definition II")
- if it has at least one redex, then it is not in II-normal form* and it's also not neutral.
There we go:
- If $t$ is a variable, it contains no more redexes and therefore we need to show (1). Trivially, a variable is in II-normal form.
- If $t$ is a lambda $lambda M$, then
- if $M$ has no more redexes, then $lambda M$ also has no more redexes, therefore we need to show (1). By the inductive hypothesis, $M$ is in II-normal form. Then by definition, $lambda M$ is also in II-normal form.
- if $M$ contains at least one more redex, then $lambda M$ also contains at least one and therefore we need to show (2). We easily see that $lambda M$ is not neutral. It remains to show that it is also not II-normal. According to the definition, $lambda M$ can be in II-normal form if a) $M$ is also in II-normal form or b) if $lambda M$ is neutral. However, regarding (a), by the induction hypothesis $M$ is not II-normal. Regarding (b), again $lambda M$ can't be neutral because by definition lambda terms are not neutral. Point (2) has been shown.
- If $t$ is an application $M,N$, we separate cases again:
- If $M$ and $N$ contain no more redexes, it is still possible for $M,N$ to be a redex. It is a redex, if $M$ is a lambda term $lambda M'$ and, therefore, $t$ is of the form $lambda M', N$. We need to show that such a term is not in II-normal form. We will assume the opposite and arrive at a contradiction. Since $t$ is an application, the only way it can be in II-normal form is if it is neutral and, by definition, $lambda M',N$ is neutral if $lambda M'$ is neutral and $N$ is II-normal. However, lambdas are not neutral. We arrived at a contradiction. Therefore, $t = lambda M', N$ is not in II-normal form.
- If $N$ or $M$ contain at least one redex, then $M,N$ also does, so we need to show (2). Again we will assume $M,N$ is in II-normal form and reach a contradiction. Since $M,N$ is in normal form, it must be the case that it is also neutral (by definition). This means that $M$ must be neutral and $N$ must be II-normal. From the induction hypothesis, if $N$ has redexes, then it is not in II-normal form and if $M$ has redexes then it is not neutral. Contradiction, hence $M,N$ is not in II-normal form.
This proves that Definition II is equivalent to "is $beta$-irreducible".
How to adapt Definition II to also account for substitution terms $t[s]$?
By the first definition, it is clear that $t[s]$ is in normal form when both $t$ and the term(s) in $s$ are. You need to append the above proof with one more inductive case for $t = M[N]$. How would you do that? How would you change Definition II so that the proof still holds?
*This is the contrapositive of saying, "if it is in II-normal form, it has no more redexes"
answered Mar 16 at 13:44
frabalafrabala
2,3241122
$endgroup$
$begingroup$
I will mark this as correct, especially when taking your comments in consideration, since both together helped me to move on to the next issue.
$endgroup$
– aphorisme
Mar 16 at 16:10
$begingroup$
@aphorisme, Appreciated :)
$endgroup$
– frabala
Mar 16 at 16:12
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%2f3150293%2frecursive-definition-of-normal-form-with-explicit-substitution%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$
Does the recursive definition make sense?
I'm guessing, this question in more formal terms would be "Are the two definitions equivalent?". To answer this, you can try to show that for every term $t$,
- if it has no more redexes, it is in II-normal form (short for "normal form by definition II")
- if it has at least one redex, then it is not in II-normal form* and it's also not neutral.
There we go:
- If $t$ is a variable, it contains no more redexes and therefore we need to show (1). Trivially, a variable is in II-normal form.
- If $t$ is a lambda $lambda M$, then
- if $M$ has no more redexes, then $lambda M$ also has no more redexes, therefore we need to show (1). By the inductive hypothesis, $M$ is in II-normal form. Then by definition, $lambda M$ is also in II-normal form.
- if $M$ contains at least one more redex, then $lambda M$ also contains at least one and therefore we need to show (2). We easily see that $lambda M$ is not neutral. It remains to show that it is also not II-normal. According to the definition, $lambda M$ can be in II-normal form if a) $M$ is also in II-normal form or b) if $lambda M$ is neutral. However, regarding (a), by the induction hypothesis $M$ is not II-normal. Regarding (b), again $lambda M$ can't be neutral because by definition lambda terms are not neutral. Point (2) has been shown.
- If $t$ is an application $M,N$, we separate cases again:
- If $M$ and $N$ contain no more redexes, it is still possible for $M,N$ to be a redex. It is a redex, if $M$ is a lambda term $lambda M'$ and, therefore, $t$ is of the form $lambda M', N$. We need to show that such a term is not in II-normal form. We will assume the opposite and arrive at a contradiction. Since $t$ is an application, the only way it can be in II-normal form is if it is neutral and, by definition, $lambda M',N$ is neutral if $lambda M'$ is neutral and $N$ is II-normal. However, lambdas are not neutral. We arrived at a contradiction. Therefore, $t = lambda M', N$ is not in II-normal form.
- If $N$ or $M$ contain at least one redex, then $M,N$ also does, so we need to show (2). Again we will assume $M,N$ is in II-normal form and reach a contradiction. Since $M,N$ is in normal form, it must be the case that it is also neutral (by definition). This means that $M$ must be neutral and $N$ must be II-normal. From the induction hypothesis, if $N$ has redexes, then it is not in II-normal form and if $M$ has redexes then it is not neutral. Contradiction, hence $M,N$ is not in II-normal form.
This proves that Definition II is equivalent to "is $beta$-irreducible".
How to adapt Definition II to also account for substitution terms $t[s]$?
By the first definition, it is clear that $t[s]$ is in normal form when both $t$ and the term(s) in $s$ are. You need to append the above proof with one more inductive case for $t = M[N]$. How would you do that? How would you change Definition II so that the proof still holds?
*This is the contrapositive of saying, "if it is in II-normal form, it has no more redexes"
answered Mar 16 at 13:44
frabalafrabala
2,3241122
$endgroup$
$begingroup$
I will mark this as correct, especially when taking your comments in consideration, since both together helped me to move on to the next issue.
$endgroup$
– aphorisme
Mar 16 at 16:10
$begingroup$
@aphorisme, Appreciated :)
$endgroup$
– frabala
Mar 16 at 16:12
add a comment |
$begingroup$
Does the recursive definition make sense?
I'm guessing, this question in more formal terms would be "Are the two definitions equivalent?". To answer this, you can try to show that for every term $t$,
- if it has no more redexes, it is in II-normal form (short for "normal form by definition II")
- if it has at least one redex, then it is not in II-normal form* and it's also not neutral.
There we go:
- If $t$ is a variable, it contains no more redexes and therefore we need to show (1). Trivially, a variable is in II-normal form.
- If $t$ is a lambda $lambda M$, then
- if $M$ has no more redexes, then $lambda M$ also has no more redexes, therefore we need to show (1). By the inductive hypothesis, $M$ is in II-normal form. Then by definition, $lambda M$ is also in II-normal form.
- if $M$ contains at least one more redex, then $lambda M$ also contains at least one and therefore we need to show (2). We easily see that $lambda M$ is not neutral. It remains to show that it is also not II-normal. According to the definition, $lambda M$ can be in II-normal form if a) $M$ is also in II-normal form or b) if $lambda M$ is neutral. However, regarding (a), by the induction hypothesis $M$ is not II-normal. Regarding (b), again $lambda M$ can't be neutral because by definition lambda terms are not neutral. Point (2) has been shown.
- If $t$ is an application $M,N$, we separate cases again:
- If $M$ and $N$ contain no more redexes, it is still possible for $M,N$ to be a redex. It is a redex, if $M$ is a lambda term $lambda M'$ and, therefore, $t$ is of the form $lambda M', N$. We need to show that such a term is not in II-normal form. We will assume the opposite and arrive at a contradiction. Since $t$ is an application, the only way it can be in II-normal form is if it is neutral and, by definition, $lambda M',N$ is neutral if $lambda M'$ is neutral and $N$ is II-normal. However, lambdas are not neutral. We arrived at a contradiction. Therefore, $t = lambda M', N$ is not in II-normal form.
- If $N$ or $M$ contain at least one redex, then $M,N$ also does, so we need to show (2). Again we will assume $M,N$ is in II-normal form and reach a contradiction. Since $M,N$ is in normal form, it must be the case that it is also neutral (by definition). This means that $M$ must be neutral and $N$ must be II-normal. From the induction hypothesis, if $N$ has redexes, then it is not in II-normal form and if $M$ has redexes then it is not neutral. Contradiction, hence $M,N$ is not in II-normal form.
This proves that Definition II is equivalent to "is $beta$-irreducible".
How to adapt Definition II to also account for substitution terms $t[s]$?
By the first definition, it is clear that $t[s]$ is in normal form when both $t$ and the term(s) in $s$ are. You need to append the above proof with one more inductive case for $t = M[N]$. How would you do that? How would you change Definition II so that the proof still holds?
*This is the contrapositive of saying, "if it is in II-normal form, it has no more redexes"
answered Mar 16 at 13:44
frabalafrabala
2,3241122
$endgroup$
$begingroup$
I will mark this as correct, especially when taking your comments in consideration, since both together helped me to move on to the next issue.
$endgroup$
– aphorisme
Mar 16 at 16:10
$begingroup$
@aphorisme, Appreciated :)
$endgroup$
– frabala
Mar 16 at 16:12
add a comment |
$begingroup$
Does the recursive definition make sense?
I'm guessing, this question in more formal terms would be "Are the two definitions equivalent?". To answer this, you can try to show that for every term $t$,
- if it has no more redexes, it is in II-normal form (short for "normal form by definition II")
- if it has at least one redex, then it is not in II-normal form* and it's also not neutral.
There we go:
- If $t$ is a variable, it contains no more redexes and therefore we need to show (1). Trivially, a variable is in II-normal form.
- If $t$ is a lambda $lambda M$, then
- if $M$ has no more redexes, then $lambda M$ also has no more redexes, therefore we need to show (1). By the inductive hypothesis, $M$ is in II-normal form. Then by definition, $lambda M$ is also in II-normal form.
- if $M$ contains at least one more redex, then $lambda M$ also contains at least one and therefore we need to show (2). We easily see that $lambda M$ is not neutral. It remains to show that it is also not II-normal. According to the definition, $lambda M$ can be in II-normal form if a) $M$ is also in II-normal form or b) if $lambda M$ is neutral. However, regarding (a), by the induction hypothesis $M$ is not II-normal. Regarding (b), again $lambda M$ can't be neutral because by definition lambda terms are not neutral. Point (2) has been shown.
- If $t$ is an application $M,N$, we separate cases again:
- If $M$ and $N$ contain no more redexes, it is still possible for $M,N$ to be a redex. It is a redex, if $M$ is a lambda term $lambda M'$ and, therefore, $t$ is of the form $lambda M', N$. We need to show that such a term is not in II-normal form. We will assume the opposite and arrive at a contradiction. Since $t$ is an application, the only way it can be in II-normal form is if it is neutral and, by definition, $lambda M',N$ is neutral if $lambda M'$ is neutral and $N$ is II-normal. However, lambdas are not neutral. We arrived at a contradiction. Therefore, $t = lambda M', N$ is not in II-normal form.
- If $N$ or $M$ contain at least one redex, then $M,N$ also does, so we need to show (2). Again we will assume $M,N$ is in II-normal form and reach a contradiction. Since $M,N$ is in normal form, it must be the case that it is also neutral (by definition). This means that $M$ must be neutral and $N$ must be II-normal. From the induction hypothesis, if $N$ has redexes, then it is not in II-normal form and if $M$ has redexes then it is not neutral. Contradiction, hence $M,N$ is not in II-normal form.
This proves that Definition II is equivalent to "is $beta$-irreducible".
How to adapt Definition II to also account for substitution terms $t[s]$?
By the first definition, it is clear that $t[s]$ is in normal form when both $t$ and the term(s) in $s$ are. You need to append the above proof with one more inductive case for $t = M[N]$. How would you do that? How would you change Definition II so that the proof still holds?
*This is the contrapositive of saying, "if it is in II-normal form, it has no more redexes"
answered Mar 16 at 13:44
frabalafrabala
2,3241122
$endgroup$
Does the recursive definition make sense?
I'm guessing, this question in more formal terms would be "Are the two definitions equivalent?". To answer this, you can try to show that for every term $t$,
- if it has no more redexes, it is in II-normal form (short for "normal form by definition II")
- if it has at least one redex, then it is not in II-normal form* and it's also not neutral.
There we go:
- If $t$ is a variable, it contains no more redexes and therefore we need to show (1). Trivially, a variable is in II-normal form.
- If $t$ is a lambda $lambda M$, then
- if $M$ has no more redexes, then $lambda M$ also has no more redexes, therefore we need to show (1). By the inductive hypothesis, $M$ is in II-normal form. Then by definition, $lambda M$ is also in II-normal form.
- if $M$ contains at least one more redex, then $lambda M$ also contains at least one and therefore we need to show (2). We easily see that $lambda M$ is not neutral. It remains to show that it is also not II-normal. According to the definition, $lambda M$ can be in II-normal form if a) $M$ is also in II-normal form or b) if $lambda M$ is neutral. However, regarding (a), by the induction hypothesis $M$ is not II-normal. Regarding (b), again $lambda M$ can't be neutral because by definition lambda terms are not neutral. Point (2) has been shown.
- If $t$ is an application $M,N$, we separate cases again:
- If $M$ and $N$ contain no more redexes, it is still possible for $M,N$ to be a redex. It is a redex, if $M$ is a lambda term $lambda M'$ and, therefore, $t$ is of the form $lambda M', N$. We need to show that such a term is not in II-normal form. We will assume the opposite and arrive at a contradiction. Since $t$ is an application, the only way it can be in II-normal form is if it is neutral and, by definition, $lambda M',N$ is neutral if $lambda M'$ is neutral and $N$ is II-normal. However, lambdas are not neutral. We arrived at a contradiction. Therefore, $t = lambda M', N$ is not in II-normal form.
- If $N$ or $M$ contain at least one redex, then $M,N$ also does, so we need to show (2). Again we will assume $M,N$ is in II-normal form and reach a contradiction. Since $M,N$ is in normal form, it must be the case that it is also neutral (by definition). This means that $M$ must be neutral and $N$ must be II-normal. From the induction hypothesis, if $N$ has redexes, then it is not in II-normal form and if $M$ has redexes then it is not neutral. Contradiction, hence $M,N$ is not in II-normal form.
This proves that Definition II is equivalent to "is $beta$-irreducible".
How to adapt Definition II to also account for substitution terms $t[s]$?
By the first definition, it is clear that $t[s]$ is in normal form when both $t$ and the term(s) in $s$ are. You need to append the above proof with one more inductive case for $t = M[N]$. How would you do that? How would you change Definition II so that the proof still holds?
*This is the contrapositive of saying, "if it is in II-normal form, it has no more redexes"
answered Mar 16 at 13:44
frabalafrabala
2,3241122
edited Mar 16 at 16:49
answered Mar 16 at 13:44
frabalafrabala
2,3241122
answered Mar 16 at 13:44
frabalafrabala
2,3241122
answered Mar 16 at 13:44
frabalafrabala
2,3241122
2,3241122
$begingroup$
I will mark this as correct, especially when taking your comments in consideration, since both together helped me to move on to the next issue.
$endgroup$
– aphorisme
Mar 16 at 16:10
$begingroup$
@aphorisme, Appreciated :)
$endgroup$
– frabala
Mar 16 at 16:12
add a comment |
$begingroup$
I will mark this as correct, especially when taking your comments in consideration, since both together helped me to move on to the next issue.
$endgroup$
– aphorisme
Mar 16 at 16:10
$begingroup$
@aphorisme, Appreciated :)
$endgroup$
– frabala
Mar 16 at 16:12
$begingroup$
I will mark this as correct, especially when taking your comments in consideration, since both together helped me to move on to the next issue.
$endgroup$
– aphorisme
Mar 16 at 16:10
$begingroup$
I will mark this as correct, especially when taking your comments in consideration, since both together helped me to move on to the next issue.
$endgroup$
– aphorisme
Mar 16 at 16:10
$begingroup$
@aphorisme, Appreciated :)
$endgroup$
– frabala
Mar 16 at 16:12
$begingroup$
@aphorisme, Appreciated :)
$endgroup$
– frabala
Mar 16 at 16:12
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%2f3150293%2frecursive-definition-of-normal-form-with-explicit-substitution%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$
Why require the terms in $s$ to be neutral? This does not allow explicit substitutions with lambdas.
$endgroup$
– frabala
Mar 16 at 14:53
$begingroup$
Well, if they are normal, then consider $s = [x leftarrow lambda M, yleftarrow N]$ where $M,N$ are normal, so every term in $s$ is normal. But then $(x y)[s]$ contains a redex. Substitution by itself is allowed to contain lambdas, but when preserving normal forms, this is not allowed.
$endgroup$
– aphorisme
Mar 16 at 14:56
$begingroup$
I don't see a redex in $(x, y)[xleftarrowlambda M, yleftarrow N]$. Aren't redexes directly applied lambdas on an argument? Do you perhaps consider another reduction rule that would justify $(x, y)[xleftarrow t_1, yleftarrow t_2]$ reducing to $(t_1 y)[yleftarrow t_2]$?
$endgroup$
– frabala
Mar 16 at 15:04
$begingroup$
Hm, maybe I've assumed things I should have mentioned. Besides adding substitution on term level, there are a few equations added as well. Especially terms $M[s]$ and $N$ are equal, if $N$ is $M$ where $M$ is substituted according to $s$ ... so in my example $(x y)[s]$ becomes $((lambda M)N)$. Okay, I see, there are a few subtelties, I cannot see since I'm too deep in.
$endgroup$
– aphorisme
Mar 16 at 15:07
$begingroup$
You want to maintain an equivalence that a value is in normal form if and only if it is irreducible. However, you add a new reduction rule for terms of the form $t[s]$. Then, if you want the equivalence preserved, in definition II terms of the form $t[s]$ should not be in normal nor neutral form. So, definition II stays as is.
$endgroup$
– frabala
Mar 16 at 15:56