3 ms·
There is a section named, "Compile your programs to formulas" Just curious, are the products of all programs formula? Worded differently, are the products of
by spynxic 10y ago
There is a section named, "Compile your programs to formulas"
Just curious, are the products of all programs formula?
Worded differently, are the products of all functions formula?
- profquail 10y agoYes - that's the Curry-Howard isomorphism: https://en.wikipedia.org/wiki/Curry–Howard_correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence
- tikhonj 10y agoI'm not sure what you mean by this question. What that lecture covers is essentially how to express an approximation of the operational semantics of a simple language as a logic formula in a very specific kind of logic (ie one of the theories supported by the Z3 SMT solver). It only supports a small number of constructs and data types, and handles infinite loops by placing an arbitrary bound on how far a program can run. It doesn't tell you anything about "all programs" or "all functions".