3 ms·
I have a tangent question: is there a formal language definition of mathematical grammar the same way there is for a programming language? If so, is it context
by gosub100 4mo ago
I have a tangent question: is there a formal language definition of mathematical grammar the same way there is for a programming language? If so, is it context sensitive or context free?
I was daydreaming about how someone would model symbolic algebra in computer code, and naively thought it would be easy, but the more I thought about it, it seems to get exponentially (pun intended) more complicated.
- 317070 4mo agoYes, people are using the programming language Lean for that, and there are a few less popular alternatives as well. Fundamentally, there is a one-to-one correspondence between mathematical proofs and programming. Proofs are isomorphic to type checking. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- gosub100 4mo agoThank you for this.