3 ms·
> A simple way to state the proposition is: in any language there are things you cannot write in the language itself: they have to be supplied by your interpret
by tromp 4y ago
> A simple way to state the proposition is: in any language there are things you cannot write in the language itself: they have to be supplied by your interpreter (or the compiler generated code which is “interpreted” by the CPU). For example you can’t write OR because if the first case is true the second case is not evaluated — you can’t write that as a function.
Not in a strict language. But it's trivial to write in a lazy language like Haskell, or the plain lambda calculus.
For a language like binary lambda calculus [1], what would be the things that you cannot write in the language itself?
[1] https://tromp.github.io/cl/Binary_lambda_calculus.html https://tromp.github.io/cl/Binary_lambda_calculus.html
- gumby 4y agoI’m not familiar with binary lambda calculus; it’s been over 35 years since I thought extensively about reflective languages. But note even in a language like Haskell the lazy semantics comes from the interpreter itself. The proposition that no language (mathematics) can represent all propositions goes back to Russel/Gödel. Perhaps the better answer is at the end of my comment: for all intents and purposes you can get essentially all the value of a reflexive language through other means, even if those means are much less elegant.
- kaba0 4y agoI’m not sure those famous math papers apply here - while programs can be proofs, they in general occupy a much larger category, don’t they? Calculable functions quickly “outgrow” mathematics.
- dumpsterlid 4y agoI mean the Curry-Howard-Lambek correspondance is that lambda calculus, proofs/logic and category theory are all just different ways of talking about the same thing for the most part
- gumby 4y agoWe’re not talking about trying to prove correctness; this is about the representational semantics of the language (a symbol system) itself.