Cfrgtkky

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
    
  
  
  
  

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.

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.