(Higher order) logic/type theory/category theory like (meta-)grammar/language/machine?
$begingroup$
TL;DR: Could you consider the relation between logic, type theory, and category theory like the relation between formal grammars (rules), formal languages (syntax), and abstract machines (semantics), and similarly, the higher order variants (of logic, etc.) as meta-equivalents (of formal grammars, etc.)?
Note: I'm not a mathematician, so most of this is self-taught. I'm a self-taught developer, so I may have missed various minor details and such. Apologies if this happened and my question wound up incomplete somehow.
I was reading up on how category theory and type theory relate, and how there's a clear duality between both of those and logic, and having some familiarity with basic formal grammar/language concepts, I started thinking of an analogy.
- Formal language theory sees languages as providing the syntax and abstract machines providing semantics. There similarly also exists a grammar, which defines the rules for building the language and for the semantics to bind to.
- Languages define the syntax, the set of strings/symbols valid within it.
- Type theory can be regarded as a formal syntactic framework for category theory, providing a set of concepts for it to work from.
- Languages can be defined based on their rules. Similarly, type theory can be defined through its logical inference rules (and generally is).
- Machines define the semantics, what each "production" does.
- Category theory can be regarded as providing a semantic framework for type theory, explaining what each concept does.
- Machines are typically defined by what they do, but the capabilities of certain classes of machines are defined by the languages they accept, with certain restrictions on their grammars. Similarly, classes of categories could be defined by the types it contains, with restrictions on which rules of logic apply. (This maps very closely to the concept of objects + morphisms.)
- Grammars define the rules applied to determine whether some set of symbols are within a language.
- Although I can't find any material explicitly stating it, it seems logic, being as rule-based as it is, fills this gap pretty well as providing a rule framework based on a syntax to define the rules.
- Grammars can "generate" languages that satisfy its rules. Similarly, logic is often used to "generate" various conclusions through their proofs, and in the case of constructive logic, is literally used to "generate" type theories and similar through strategic rule definitions.
- Higher order logic/type theory/category theory extends this to basically generate such logic/type theories/category theories, almost as templates.
- This is analogous to meta-grammars, meta-languages, and hypermachines/machines that implement machines.*
- Similarly, this can be narrowed to intuitionistic propositional logic/simply typed lambda calculus/Cartesian closed categories due to the Curry-Howard-Lambek correspondence
- This is analogous to the hierarchy of non-recursive grammars/finite languages/DAFSA
- This is analogous to the hierarchy of non-recursive grammars/finite languages/DAFSA
So, in a sense, if I'm correct with my reasoning,
$$
begin{matrix}
text{(higher order) logic} \
text{(meta-) rules} \
text{(meta-) grammar}
end{matrix}
Leftrightarrow
begin{matrix}
text{(higher order) type theory} \
text{(meta-) syntax} \
text{(meta-) language}
end{matrix}
Leftrightarrow
begin{matrix}
text{(higher order) category theory} \
text{(meta-) semantics} \
text{(meta-) machine}
end{matrix}
$$
?
Or am I missing something?
Also, by any chance, where could I find some authors/researchers that could help me better understand this relation?
* It'd be nice if Wikipedia actually made these remotely accessible from anywhere else short of hard-to-discover Google searches.
logic soft-question category-theory formal-languages type-theory
asked Feb 4 '18 at 14:55
Isiah MeadowsIsiah Meadows
11510
$endgroup$
add a comment |
$begingroup$
TL;DR: Could you consider the relation between logic, type theory, and category theory like the relation between formal grammars (rules), formal languages (syntax), and abstract machines (semantics), and similarly, the higher order variants (of logic, etc.) as meta-equivalents (of formal grammars, etc.)?
Note: I'm not a mathematician, so most of this is self-taught. I'm a self-taught developer, so I may have missed various minor details and such. Apologies if this happened and my question wound up incomplete somehow.
I was reading up on how category theory and type theory relate, and how there's a clear duality between both of those and logic, and having some familiarity with basic formal grammar/language concepts, I started thinking of an analogy.
- Formal language theory sees languages as providing the syntax and abstract machines providing semantics. There similarly also exists a grammar, which defines the rules for building the language and for the semantics to bind to.
- Languages define the syntax, the set of strings/symbols valid within it.
- Type theory can be regarded as a formal syntactic framework for category theory, providing a set of concepts for it to work from.
- Languages can be defined based on their rules. Similarly, type theory can be defined through its logical inference rules (and generally is).
- Machines define the semantics, what each "production" does.
- Category theory can be regarded as providing a semantic framework for type theory, explaining what each concept does.
- Machines are typically defined by what they do, but the capabilities of certain classes of machines are defined by the languages they accept, with certain restrictions on their grammars. Similarly, classes of categories could be defined by the types it contains, with restrictions on which rules of logic apply. (This maps very closely to the concept of objects + morphisms.)
- Grammars define the rules applied to determine whether some set of symbols are within a language.
- Although I can't find any material explicitly stating it, it seems logic, being as rule-based as it is, fills this gap pretty well as providing a rule framework based on a syntax to define the rules.
- Grammars can "generate" languages that satisfy its rules. Similarly, logic is often used to "generate" various conclusions through their proofs, and in the case of constructive logic, is literally used to "generate" type theories and similar through strategic rule definitions.
- Higher order logic/type theory/category theory extends this to basically generate such logic/type theories/category theories, almost as templates.
- This is analogous to meta-grammars, meta-languages, and hypermachines/machines that implement machines.*
- Similarly, this can be narrowed to intuitionistic propositional logic/simply typed lambda calculus/Cartesian closed categories due to the Curry-Howard-Lambek correspondence
- This is analogous to the hierarchy of non-recursive grammars/finite languages/DAFSA
- This is analogous to the hierarchy of non-recursive grammars/finite languages/DAFSA
So, in a sense, if I'm correct with my reasoning,
$$
begin{matrix}
text{(higher order) logic} \
text{(meta-) rules} \
text{(meta-) grammar}
end{matrix}
Leftrightarrow
begin{matrix}
text{(higher order) type theory} \
text{(meta-) syntax} \
text{(meta-) language}
end{matrix}
Leftrightarrow
begin{matrix}
text{(higher order) category theory} \
text{(meta-) semantics} \
text{(meta-) machine}
end{matrix}
$$
?
Or am I missing something?
Also, by any chance, where could I find some authors/researchers that could help me better understand this relation?
* It'd be nice if Wikipedia actually made these remotely accessible from anywhere else short of hard-to-discover Google searches.
logic soft-question category-theory formal-languages type-theory
asked Feb 4 '18 at 14:55
Isiah MeadowsIsiah Meadows
11510
$endgroup$
$begingroup$
If my tags are wrong, or if other tags need added (since this is a pretty broad subject matter I'm referring to), please feel free to add them. (I could only add 5 initially, and I'm not quite sure that's enough for this question.) Also, I'm not a math major, I'm a software developer who enjoys some occasional highly-theoretical mathematics, so I'm still learning as I go. (This also means I didn't necessarily get all the formal education to know all this by heart.)
$endgroup$
– Isiah Meadows
Feb 4 '18 at 14:59
1
$begingroup$
This sounds like computational trinitarianism, if you want a Google target.
$endgroup$
– Kevin Carlson
Feb 4 '18 at 21:46
$begingroup$
Okay. I found that in one of the links, but I wasn't sure how much I could find on Google. Also, my question is geared more towards relating it to formal language theory, as they seem "isomorphic" to one another at a certain level of abstraction. (I know that's not technically correct, but you probably get my analogy.)
$endgroup$
– Isiah Meadows
Feb 5 '18 at 5:48
1
$begingroup$
Higher-order logic has nothing to do with higher category theory. Instead, higher order logic corresponds to topos theory.
$endgroup$
– Hurkyl
Feb 13 '18 at 22:43
add a comment |
$begingroup$
TL;DR: Could you consider the relation between logic, type theory, and category theory like the relation between formal grammars (rules), formal languages (syntax), and abstract machines (semantics), and similarly, the higher order variants (of logic, etc.) as meta-equivalents (of formal grammars, etc.)?
Note: I'm not a mathematician, so most of this is self-taught. I'm a self-taught developer, so I may have missed various minor details and such. Apologies if this happened and my question wound up incomplete somehow.
I was reading up on how category theory and type theory relate, and how there's a clear duality between both of those and logic, and having some familiarity with basic formal grammar/language concepts, I started thinking of an analogy.
- Formal language theory sees languages as providing the syntax and abstract machines providing semantics. There similarly also exists a grammar, which defines the rules for building the language and for the semantics to bind to.
- Languages define the syntax, the set of strings/symbols valid within it.
- Type theory can be regarded as a formal syntactic framework for category theory, providing a set of concepts for it to work from.
- Languages can be defined based on their rules. Similarly, type theory can be defined through its logical inference rules (and generally is).
- Machines define the semantics, what each "production" does.
- Category theory can be regarded as providing a semantic framework for type theory, explaining what each concept does.
- Machines are typically defined by what they do, but the capabilities of certain classes of machines are defined by the languages they accept, with certain restrictions on their grammars. Similarly, classes of categories could be defined by the types it contains, with restrictions on which rules of logic apply. (This maps very closely to the concept of objects + morphisms.)
- Grammars define the rules applied to determine whether some set of symbols are within a language.
- Although I can't find any material explicitly stating it, it seems logic, being as rule-based as it is, fills this gap pretty well as providing a rule framework based on a syntax to define the rules.
- Grammars can "generate" languages that satisfy its rules. Similarly, logic is often used to "generate" various conclusions through their proofs, and in the case of constructive logic, is literally used to "generate" type theories and similar through strategic rule definitions.
- Higher order logic/type theory/category theory extends this to basically generate such logic/type theories/category theories, almost as templates.
- This is analogous to meta-grammars, meta-languages, and hypermachines/machines that implement machines.*
- Similarly, this can be narrowed to intuitionistic propositional logic/simply typed lambda calculus/Cartesian closed categories due to the Curry-Howard-Lambek correspondence
- This is analogous to the hierarchy of non-recursive grammars/finite languages/DAFSA
- This is analogous to the hierarchy of non-recursive grammars/finite languages/DAFSA
So, in a sense, if I'm correct with my reasoning,
$$
begin{matrix}
text{(higher order) logic} \
text{(meta-) rules} \
text{(meta-) grammar}
end{matrix}
Leftrightarrow
begin{matrix}
text{(higher order) type theory} \
text{(meta-) syntax} \
text{(meta-) language}
end{matrix}
Leftrightarrow
begin{matrix}
text{(higher order) category theory} \
text{(meta-) semantics} \
text{(meta-) machine}
end{matrix}
$$
?
Or am I missing something?
Also, by any chance, where could I find some authors/researchers that could help me better understand this relation?
* It'd be nice if Wikipedia actually made these remotely accessible from anywhere else short of hard-to-discover Google searches.
logic soft-question category-theory formal-languages type-theory
asked Feb 4 '18 at 14:55
Isiah MeadowsIsiah Meadows
11510
$endgroup$
TL;DR: Could you consider the relation between logic, type theory, and category theory like the relation between formal grammars (rules), formal languages (syntax), and abstract machines (semantics), and similarly, the higher order variants (of logic, etc.) as meta-equivalents (of formal grammars, etc.)?
Note: I'm not a mathematician, so most of this is self-taught. I'm a self-taught developer, so I may have missed various minor details and such. Apologies if this happened and my question wound up incomplete somehow.
I was reading up on how category theory and type theory relate, and how there's a clear duality between both of those and logic, and having some familiarity with basic formal grammar/language concepts, I started thinking of an analogy.
- Formal language theory sees languages as providing the syntax and abstract machines providing semantics. There similarly also exists a grammar, which defines the rules for building the language and for the semantics to bind to.
- Languages define the syntax, the set of strings/symbols valid within it.
- Type theory can be regarded as a formal syntactic framework for category theory, providing a set of concepts for it to work from.
- Languages can be defined based on their rules. Similarly, type theory can be defined through its logical inference rules (and generally is).
- Machines define the semantics, what each "production" does.
- Category theory can be regarded as providing a semantic framework for type theory, explaining what each concept does.
- Machines are typically defined by what they do, but the capabilities of certain classes of machines are defined by the languages they accept, with certain restrictions on their grammars. Similarly, classes of categories could be defined by the types it contains, with restrictions on which rules of logic apply. (This maps very closely to the concept of objects + morphisms.)
- Grammars define the rules applied to determine whether some set of symbols are within a language.
- Although I can't find any material explicitly stating it, it seems logic, being as rule-based as it is, fills this gap pretty well as providing a rule framework based on a syntax to define the rules.
- Grammars can "generate" languages that satisfy its rules. Similarly, logic is often used to "generate" various conclusions through their proofs, and in the case of constructive logic, is literally used to "generate" type theories and similar through strategic rule definitions.
- Higher order logic/type theory/category theory extends this to basically generate such logic/type theories/category theories, almost as templates.
- This is analogous to meta-grammars, meta-languages, and hypermachines/machines that implement machines.*
- Similarly, this can be narrowed to intuitionistic propositional logic/simply typed lambda calculus/Cartesian closed categories due to the Curry-Howard-Lambek correspondence
- This is analogous to the hierarchy of non-recursive grammars/finite languages/DAFSA
- This is analogous to the hierarchy of non-recursive grammars/finite languages/DAFSA
So, in a sense, if I'm correct with my reasoning,
$$
begin{matrix}
text{(higher order) logic} \
text{(meta-) rules} \
text{(meta-) grammar}
end{matrix}
Leftrightarrow
begin{matrix}
text{(higher order) type theory} \
text{(meta-) syntax} \
text{(meta-) language}
end{matrix}
Leftrightarrow
begin{matrix}
text{(higher order) category theory} \
text{(meta-) semantics} \
text{(meta-) machine}
end{matrix}
$$
?
Or am I missing something?
Also, by any chance, where could I find some authors/researchers that could help me better understand this relation?
* It'd be nice if Wikipedia actually made these remotely accessible from anywhere else short of hard-to-discover Google searches.
logic soft-question category-theory formal-languages type-theory
logic soft-question category-theory formal-languages type-theory
asked Feb 4 '18 at 14:55
Isiah MeadowsIsiah Meadows
11510
asked Feb 4 '18 at 14:55
Isiah MeadowsIsiah Meadows
11510
edited Feb 13 '18 at 9:07
Isiah Meadows
asked Feb 4 '18 at 14:55
Isiah MeadowsIsiah Meadows
11510
asked Feb 4 '18 at 14:55
Isiah MeadowsIsiah Meadows
11510
asked Feb 4 '18 at 14:55
Isiah MeadowsIsiah Meadows
11510
11510
$begingroup$
If my tags are wrong, or if other tags need added (since this is a pretty broad subject matter I'm referring to), please feel free to add them. (I could only add 5 initially, and I'm not quite sure that's enough for this question.) Also, I'm not a math major, I'm a software developer who enjoys some occasional highly-theoretical mathematics, so I'm still learning as I go. (This also means I didn't necessarily get all the formal education to know all this by heart.)
$endgroup$
– Isiah Meadows
Feb 4 '18 at 14:59
1
$begingroup$
This sounds like computational trinitarianism, if you want a Google target.
$endgroup$
– Kevin Carlson
Feb 4 '18 at 21:46
$begingroup$
Okay. I found that in one of the links, but I wasn't sure how much I could find on Google. Also, my question is geared more towards relating it to formal language theory, as they seem "isomorphic" to one another at a certain level of abstraction. (I know that's not technically correct, but you probably get my analogy.)
$endgroup$
– Isiah Meadows
Feb 5 '18 at 5:48
1
$begingroup$
Higher-order logic has nothing to do with higher category theory. Instead, higher order logic corresponds to topos theory.
$endgroup$
– Hurkyl
Feb 13 '18 at 22:43
add a comment |
$begingroup$
If my tags are wrong, or if other tags need added (since this is a pretty broad subject matter I'm referring to), please feel free to add them. (I could only add 5 initially, and I'm not quite sure that's enough for this question.) Also, I'm not a math major, I'm a software developer who enjoys some occasional highly-theoretical mathematics, so I'm still learning as I go. (This also means I didn't necessarily get all the formal education to know all this by heart.)
$endgroup$
– Isiah Meadows
Feb 4 '18 at 14:59
1
$begingroup$
This sounds like computational trinitarianism, if you want a Google target.
$endgroup$
– Kevin Carlson
Feb 4 '18 at 21:46
$begingroup$
Okay. I found that in one of the links, but I wasn't sure how much I could find on Google. Also, my question is geared more towards relating it to formal language theory, as they seem "isomorphic" to one another at a certain level of abstraction. (I know that's not technically correct, but you probably get my analogy.)
$endgroup$
– Isiah Meadows
Feb 5 '18 at 5:48
1
$begingroup$
Higher-order logic has nothing to do with higher category theory. Instead, higher order logic corresponds to topos theory.
$endgroup$
– Hurkyl
Feb 13 '18 at 22:43
$begingroup$
If my tags are wrong, or if other tags need added (since this is a pretty broad subject matter I'm referring to), please feel free to add them. (I could only add 5 initially, and I'm not quite sure that's enough for this question.) Also, I'm not a math major, I'm a software developer who enjoys some occasional highly-theoretical mathematics, so I'm still learning as I go. (This also means I didn't necessarily get all the formal education to know all this by heart.)
$endgroup$
– Isiah Meadows
Feb 4 '18 at 14:59
$begingroup$
If my tags are wrong, or if other tags need added (since this is a pretty broad subject matter I'm referring to), please feel free to add them. (I could only add 5 initially, and I'm not quite sure that's enough for this question.) Also, I'm not a math major, I'm a software developer who enjoys some occasional highly-theoretical mathematics, so I'm still learning as I go. (This also means I didn't necessarily get all the formal education to know all this by heart.)
$endgroup$
– Isiah Meadows
Feb 4 '18 at 14:59
1
1
$begingroup$
This sounds like computational trinitarianism, if you want a Google target.
$endgroup$
– Kevin Carlson
Feb 4 '18 at 21:46
$begingroup$
This sounds like computational trinitarianism, if you want a Google target.
$endgroup$
– Kevin Carlson
Feb 4 '18 at 21:46
$begingroup$
Okay. I found that in one of the links, but I wasn't sure how much I could find on Google. Also, my question is geared more towards relating it to formal language theory, as they seem "isomorphic" to one another at a certain level of abstraction. (I know that's not technically correct, but you probably get my analogy.)
$endgroup$
– Isiah Meadows
Feb 5 '18 at 5:48
$begingroup$
Okay. I found that in one of the links, but I wasn't sure how much I could find on Google. Also, my question is geared more towards relating it to formal language theory, as they seem "isomorphic" to one another at a certain level of abstraction. (I know that's not technically correct, but you probably get my analogy.)
$endgroup$
– Isiah Meadows
Feb 5 '18 at 5:48
1
1
$begingroup$
Higher-order logic has nothing to do with higher category theory. Instead, higher order logic corresponds to topos theory.
$endgroup$
– Hurkyl
Feb 13 '18 at 22:43
$begingroup$
Higher-order logic has nothing to do with higher category theory. Instead, higher order logic corresponds to topos theory.
$endgroup$
– Hurkyl
Feb 13 '18 at 22:43
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
I am not entirely sure I have completely understood your question but I will try to give me 2 cents.
It is true that you can regard logics and type theories as some sort of grammars. The elements of the languages generated by these grammars are called judgments: they will be logical judgments in case you are dealing with logics and they will be typing judgements or equality-judgments in case your dealing with type theories.
The relation between logics and type theories is different from the one between grammars and languages: logics do not generate type theories, they are both grammars.
The Curry-Howard theorem establishes an isomorphism between the grammar intuitionistic propositional calculus and the grammar simply typed lambda calculus and between their languages ... though more exactly this isomorphism regards just the typing rules/judgment of simply typed lambda calculus.
Similarly there are generalizations of Curry Howard isomorphism between other logics and type theories. Again these isomorphisms relate the grammars-logics with the grammar type theories.
About the semantics: usually abstract machines are a way to provide an operational semantics for a language. Category theory provides a semantics for logics and type theories, but it is a denotational semantics which differs for the operational ones.
I hope this addresses your doubts, if you need additional details or some clarifications feel free to ask.
answered Feb 14 '18 at 19:53
Giorgio MossaGiorgio Mossa
14k11749
$endgroup$
$begingroup$
So types are more a type of logic?
$endgroup$
– Isiah Meadows
Feb 14 '18 at 22:00
$begingroup$
More or less yes, depending what you mean by that.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 0:04
1
$begingroup$
@IsiahMeadows more exactly I would dare to say that type theories are logic with proof relevance, i.e. logics where we do not regard proofs as equivalent: the equality judgments in type theories can be regarded as statements saying that certain proofs (which correspond to terms of type theories) are equal.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 10:30
$begingroup$
Thanks! (filler text)
$endgroup$
– Isiah Meadows
Feb 15 '18 at 11:09
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%2f2635625%2fhigher-order-logic-type-theory-category-theory-like-meta-grammar-language-ma%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$
I am not entirely sure I have completely understood your question but I will try to give me 2 cents.
It is true that you can regard logics and type theories as some sort of grammars. The elements of the languages generated by these grammars are called judgments: they will be logical judgments in case you are dealing with logics and they will be typing judgements or equality-judgments in case your dealing with type theories.
The relation between logics and type theories is different from the one between grammars and languages: logics do not generate type theories, they are both grammars.
The Curry-Howard theorem establishes an isomorphism between the grammar intuitionistic propositional calculus and the grammar simply typed lambda calculus and between their languages ... though more exactly this isomorphism regards just the typing rules/judgment of simply typed lambda calculus.
Similarly there are generalizations of Curry Howard isomorphism between other logics and type theories. Again these isomorphisms relate the grammars-logics with the grammar type theories.
About the semantics: usually abstract machines are a way to provide an operational semantics for a language. Category theory provides a semantics for logics and type theories, but it is a denotational semantics which differs for the operational ones.
I hope this addresses your doubts, if you need additional details or some clarifications feel free to ask.
answered Feb 14 '18 at 19:53
Giorgio MossaGiorgio Mossa
14k11749
$endgroup$
$begingroup$
So types are more a type of logic?
$endgroup$
– Isiah Meadows
Feb 14 '18 at 22:00
$begingroup$
More or less yes, depending what you mean by that.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 0:04
1
$begingroup$
@IsiahMeadows more exactly I would dare to say that type theories are logic with proof relevance, i.e. logics where we do not regard proofs as equivalent: the equality judgments in type theories can be regarded as statements saying that certain proofs (which correspond to terms of type theories) are equal.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 10:30
$begingroup$
Thanks! (filler text)
$endgroup$
– Isiah Meadows
Feb 15 '18 at 11:09
add a comment |
$begingroup$
I am not entirely sure I have completely understood your question but I will try to give me 2 cents.
It is true that you can regard logics and type theories as some sort of grammars. The elements of the languages generated by these grammars are called judgments: they will be logical judgments in case you are dealing with logics and they will be typing judgements or equality-judgments in case your dealing with type theories.
The relation between logics and type theories is different from the one between grammars and languages: logics do not generate type theories, they are both grammars.
The Curry-Howard theorem establishes an isomorphism between the grammar intuitionistic propositional calculus and the grammar simply typed lambda calculus and between their languages ... though more exactly this isomorphism regards just the typing rules/judgment of simply typed lambda calculus.
Similarly there are generalizations of Curry Howard isomorphism between other logics and type theories. Again these isomorphisms relate the grammars-logics with the grammar type theories.
About the semantics: usually abstract machines are a way to provide an operational semantics for a language. Category theory provides a semantics for logics and type theories, but it is a denotational semantics which differs for the operational ones.
I hope this addresses your doubts, if you need additional details or some clarifications feel free to ask.
answered Feb 14 '18 at 19:53
Giorgio MossaGiorgio Mossa
14k11749
$endgroup$
$begingroup$
So types are more a type of logic?
$endgroup$
– Isiah Meadows
Feb 14 '18 at 22:00
$begingroup$
More or less yes, depending what you mean by that.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 0:04
1
$begingroup$
@IsiahMeadows more exactly I would dare to say that type theories are logic with proof relevance, i.e. logics where we do not regard proofs as equivalent: the equality judgments in type theories can be regarded as statements saying that certain proofs (which correspond to terms of type theories) are equal.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 10:30
$begingroup$
Thanks! (filler text)
$endgroup$
– Isiah Meadows
Feb 15 '18 at 11:09
add a comment |
$begingroup$
I am not entirely sure I have completely understood your question but I will try to give me 2 cents.
It is true that you can regard logics and type theories as some sort of grammars. The elements of the languages generated by these grammars are called judgments: they will be logical judgments in case you are dealing with logics and they will be typing judgements or equality-judgments in case your dealing with type theories.
The relation between logics and type theories is different from the one between grammars and languages: logics do not generate type theories, they are both grammars.
The Curry-Howard theorem establishes an isomorphism between the grammar intuitionistic propositional calculus and the grammar simply typed lambda calculus and between their languages ... though more exactly this isomorphism regards just the typing rules/judgment of simply typed lambda calculus.
Similarly there are generalizations of Curry Howard isomorphism between other logics and type theories. Again these isomorphisms relate the grammars-logics with the grammar type theories.
About the semantics: usually abstract machines are a way to provide an operational semantics for a language. Category theory provides a semantics for logics and type theories, but it is a denotational semantics which differs for the operational ones.
I hope this addresses your doubts, if you need additional details or some clarifications feel free to ask.
answered Feb 14 '18 at 19:53
Giorgio MossaGiorgio Mossa
14k11749
$endgroup$
I am not entirely sure I have completely understood your question but I will try to give me 2 cents.
It is true that you can regard logics and type theories as some sort of grammars. The elements of the languages generated by these grammars are called judgments: they will be logical judgments in case you are dealing with logics and they will be typing judgements or equality-judgments in case your dealing with type theories.
The relation between logics and type theories is different from the one between grammars and languages: logics do not generate type theories, they are both grammars.
The Curry-Howard theorem establishes an isomorphism between the grammar intuitionistic propositional calculus and the grammar simply typed lambda calculus and between their languages ... though more exactly this isomorphism regards just the typing rules/judgment of simply typed lambda calculus.
Similarly there are generalizations of Curry Howard isomorphism between other logics and type theories. Again these isomorphisms relate the grammars-logics with the grammar type theories.
About the semantics: usually abstract machines are a way to provide an operational semantics for a language. Category theory provides a semantics for logics and type theories, but it is a denotational semantics which differs for the operational ones.
I hope this addresses your doubts, if you need additional details or some clarifications feel free to ask.
answered Feb 14 '18 at 19:53
Giorgio MossaGiorgio Mossa
14k11749
edited Nov 25 '18 at 12:54
answered Feb 14 '18 at 19:53
Giorgio MossaGiorgio Mossa
14k11749
answered Feb 14 '18 at 19:53
Giorgio MossaGiorgio Mossa
14k11749
answered Feb 14 '18 at 19:53
Giorgio MossaGiorgio Mossa
14k11749
14k11749
$begingroup$
So types are more a type of logic?
$endgroup$
– Isiah Meadows
Feb 14 '18 at 22:00
$begingroup$
More or less yes, depending what you mean by that.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 0:04
1
$begingroup$
@IsiahMeadows more exactly I would dare to say that type theories are logic with proof relevance, i.e. logics where we do not regard proofs as equivalent: the equality judgments in type theories can be regarded as statements saying that certain proofs (which correspond to terms of type theories) are equal.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 10:30
$begingroup$
Thanks! (filler text)
$endgroup$
– Isiah Meadows
Feb 15 '18 at 11:09
add a comment |
$begingroup$
So types are more a type of logic?
$endgroup$
– Isiah Meadows
Feb 14 '18 at 22:00
$begingroup$
More or less yes, depending what you mean by that.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 0:04
1
$begingroup$
@IsiahMeadows more exactly I would dare to say that type theories are logic with proof relevance, i.e. logics where we do not regard proofs as equivalent: the equality judgments in type theories can be regarded as statements saying that certain proofs (which correspond to terms of type theories) are equal.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 10:30
$begingroup$
Thanks! (filler text)
$endgroup$
– Isiah Meadows
Feb 15 '18 at 11:09
$begingroup$
So types are more a type of logic?
$endgroup$
– Isiah Meadows
Feb 14 '18 at 22:00
$begingroup$
So types are more a type of logic?
$endgroup$
– Isiah Meadows
Feb 14 '18 at 22:00
$begingroup$
More or less yes, depending what you mean by that.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 0:04
$begingroup$
More or less yes, depending what you mean by that.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 0:04
1
1
$begingroup$
@IsiahMeadows more exactly I would dare to say that type theories are logic with proof relevance, i.e. logics where we do not regard proofs as equivalent: the equality judgments in type theories can be regarded as statements saying that certain proofs (which correspond to terms of type theories) are equal.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 10:30
$begingroup$
@IsiahMeadows more exactly I would dare to say that type theories are logic with proof relevance, i.e. logics where we do not regard proofs as equivalent: the equality judgments in type theories can be regarded as statements saying that certain proofs (which correspond to terms of type theories) are equal.
$endgroup$
– Giorgio Mossa
Feb 15 '18 at 10:30
$begingroup$
Thanks! (filler text)
$endgroup$
– Isiah Meadows
Feb 15 '18 at 11:09
$begingroup$
Thanks! (filler text)
$endgroup$
– Isiah Meadows
Feb 15 '18 at 11:09
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%2f2635625%2fhigher-order-logic-type-theory-category-theory-like-meta-grammar-language-ma%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$
If my tags are wrong, or if other tags need added (since this is a pretty broad subject matter I'm referring to), please feel free to add them. (I could only add 5 initially, and I'm not quite sure that's enough for this question.) Also, I'm not a math major, I'm a software developer who enjoys some occasional highly-theoretical mathematics, so I'm still learning as I go. (This also means I didn't necessarily get all the formal education to know all this by heart.)
$endgroup$
– Isiah Meadows
Feb 4 '18 at 14:59
1
$begingroup$
This sounds like computational trinitarianism, if you want a Google target.
$endgroup$
– Kevin Carlson
Feb 4 '18 at 21:46
$begingroup$
Okay. I found that in one of the links, but I wasn't sure how much I could find on Google. Also, my question is geared more towards relating it to formal language theory, as they seem "isomorphic" to one another at a certain level of abstraction. (I know that's not technically correct, but you probably get my analogy.)
$endgroup$
– Isiah Meadows
Feb 5 '18 at 5:48
1
$begingroup$
Higher-order logic has nothing to do with higher category theory. Instead, higher order logic corresponds to topos theory.
$endgroup$
– Hurkyl
Feb 13 '18 at 22:43