|
|
|
|
|
|
by gosub100
8 days 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. |
|
|
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_correspon...