Wed Mar 17 08:37:48 CET 2010
Mathematical Logic and Compilation
I'm trying to get some intuition straight about specification by
compiler. I don't find what I'm looking for on the web, so I guess
it's ``obvious'' ;)
In formal mathematics and logic, you have syntax (s) and inference
rules (s1,s2,... -| s) that allow the construction of new syntax.
To alleviate the tedium of working with such a low-level substrate,
one allows the construction of (informal, finitistic) mathematical
structure that talks about manipulation of formula and proofs.
I.e. that talks about the existence of proofs using constructive
methods: algorithms to construct a proof.
Now, in compiler construction one works the other way around:
* One starts with a physical model (i.e. an electronic circuit).
This can be abstracted by a mathematical (semantic) model.
* The objective is then to derive a formal system (syntax and code
transformation rules) and an interpretation such that the semantic
model is preserved.
I probably need to look at Model Theory and Proof Theory.
( I need to grow some more hair on my chest. )