7 ms·

I'm still a little unclear on what we would achieve by making the language 'complete.' I get that being able to check for non-termination would be useful—but is

I'm still a little unclear on what we would achieve by making the language 'complete.' I get that being able to check for non-termination would be useful—but is there more? The paper opens with: The driving idea of functional programming is to make programming more closely related to mathematics. From a paper by John Backus: Associated with the functional style of programming is an algebra of programs whose variables range over programs and whose operations are combining forms. This algebra can be used to transform programs and to solve equations whose “unknowns” are programs in much the same way one transforms equations in high school algebra. Are they talking about the same thing here? Also, are there advantages to having such an algebra of programs outside of correctness verification?

pash 10y ago
> Are they talking about the same thing here? Yes, they're talking about roughly the same thing. The kernel of the idea is called "equational reasoning", which exploits the key mathematical characteristic of functional programs, that they are referentially transparent [0]. > Also, are there advantages to having such an algebra of programs outside of correctness verification? Proving correctness is a big one, but you can also use these techniques to derive more sophisticated algorithms from a naive (but correct) first implementation. For an example, see section 4 on the implementation of an efficient minimax algorithm in a short paper by Richard Bird [1]. (You will have to read some of the previous sections to understand the example.) If that piques your interest, Bird's introductory book on functional programming written with Philip Wadler [2] introduces the technique, which is usually called "program calculation". (Though published in 1988, their book remains a great introduction to functional programming.) If you really want to go off the deep end, Jeremy Gibbons's extensive lectures notes, published as a book chapter [3], are the best source I know. (Beware: here be category theory.) 0. https://en.m.wikipedia.org/wiki/Referential_transparency https://en.m.wikipedia.org/wiki/Referential_transparency 1. R. Bird (1988), "Algebraic identities for program calculation", http://comjnl.oxfordjournals.org/content/32/2/122.full.pdf http://comjnl.oxfordjournals.org/content/32/2/122.full.pdf [PDF] 2. R. Bird and P. Wadler (1988), Introduction to Functional Programming. It's out of print and hard copies are scarce, but a scan is available at https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Introduction%20to%20Functional%20Programming.1ed.pdf https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Intro... [PDF] 3. J. Gibbons (2002), "Calculating Functional Programs, http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-calcfp.pdf http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-ca... [PDF]
- peternicky 10y ago
  Thank you for these resources.
- pron 10y ago
  > Proving correctness is a big one Totality does in no way make proving correctness easier in practice. See http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c... Totality really mostly helps when using typed programming languages as proofs of general (non-executable) mathematical theorems via propositions-as-types. Without it, the logic will be inconsistent. For actual programs, though, it makes little difference.
  - deleted 10y ago
    [deleted]
drostie 10y ago
> I get that being able to check for non-termination would be useful—but is there more? It's not just that "there is more", it's that there is everything. The halting problem which we're talking about here is actually easily generalizable into a set of generic theorems about static analysis of programs in general. The usual first step is to prove the first incompleteness theorem (no axiom system proves all of the interesting facts about the integers), then modify that into a proof of the second incompleteness theorem (that every logic which proves its own consistency must be inconsistent). But it goes way further than that to Rice's theorem: every nontrivial semantic property of a computer program is undecidable. Put another way, the only way for the compiler to know that something is true is for there to be a really simple up-front convention which makes it true. Suppose you want to make sure, statically, that you never dereference a null pointer. This says that the only way a compiler could ever be strong enough to prove this is if it's syntactically impossible to create a null pointer in the language in the first place, so that it's a "trivial property" of all programs that they never dereference null pointers. Suppose you want to prove that a certain block of code is the fastest possible code which does a certain thing. The only ways to do this require the language to "normalize" all of its expressions so that there is only one block of code for everything you want to do. If there's more than one way to do it, then the analysis "is this the fastest code?" is nontrivial and you can't prove it! (You can always get heuristics of course to try to cover the most common cases, but your heuristics will never cover everything you want.) Suppose Microsoft wants to fix Word and Excel's macro systems to a new form that cannot contain viruses: the only way to do that is if the macro system is either (a) Turing-incomplete, so that you can analyze its programs, or else (b) unable to do the virusy things that you're worried about in the first place. Otherwise there will always be a macro-virus which passes the virus-checker.
- skybrian 10y ago
  In theory, sure. In practice, a program that takes a century to run is indistinguishable from a non-terminating program. If you prove a macro is safe by trying every possible combination then it could very well take that long. And we usually don't wait that long. A function that executes when loading a web page times out in the order of seconds. Once you have deadlines, all bets are off - the function is not deterministic for any large enough input. Equational reasoning does not preserve performance - it could cause a program that previously ran fast enough to time out. So, knowing that function terminates seems only theoretically useful. It doesn't tell us whether a program change is really safe. It would be more useful to put some kind of bound on the resources a function can consume. In Etherium's language, there is a concept of "gas" which is an abstract limit on how much work a function can do. (The advantage over a timeout is that it's not machine-specific.) I sometimes wonder if anyone has applied this concept to functional programming? Could we define a language so that it uses static analysis to maintain guarantees about a function's use of gas?

pash 10y ago

> Are they talking about the same thing here? Yes, they're talking about roughly the same thing. The kernel of the idea is called "equational reasoning", which exploits the key mathematical characteristic of functional programs, that they are referentially transparent [0]. > Also, are there advantages to having such an algebra of programs outside of correctness verification? Proving correctness is a big one, but you can also use these techniques to derive more sophisticated algorithms from a naive (but correct) first implementation. For an example, see section 4 on the implementation of an efficient minimax algorithm in a short paper by Richard Bird [1]. (You will have to read some of the previous sections to understand the example.) If that piques your interest, Bird's introductory book on functional programming written with Philip Wadler [2] introduces the technique, which is usually called "program calculation". (Though published in 1988, their book remains a great introduction to functional programming.) If you really want to go off the deep end, Jeremy Gibbons's extensive lectures notes, published as a book chapter [3], are the best source I know. (Beware: here be category theory.) 0. https://en.m.wikipedia.org/wiki/Referential_transparency https://en.m.wikipedia.org/wiki/Referential_transparency 1. R. Bird (1988), "Algebraic identities for program calculation", http://comjnl.oxfordjournals.org/content/32/2/122.full.pdf http://comjnl.oxfordjournals.org/content/32/2/122.full.pdf [PDF] 2. R. Bird and P. Wadler (1988), Introduction to Functional Programming. It's out of print and hard copies are scarce, but a scan is available at https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Introduction%20to%20Functional%20Programming.1ed.pdf https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Intro... [PDF] 3. J. Gibbons (2002), "Calculating Functional Programs, http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-calcfp.pdf http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-ca... [PDF]

peternicky 10y ago
Thank you for these resources.
pron 10y ago
> Proving correctness is a big one Totality does in no way make proving correctness easier in practice. See http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c... Totality really mostly helps when using typed programming languages as proofs of general (non-executable) mathematical theorems via propositions-as-types. Without it, the logic will be inconsistent. For actual programs, though, it makes little difference.
- deleted 10y ago
  [deleted]

drostie 10y ago

> I get that being able to check for non-termination would be useful—but is there more? It's not just that "there is more", it's that there is everything. The halting problem which we're talking about here is actually easily generalizable into a set of generic theorems about static analysis of programs in general. The usual first step is to prove the first incompleteness theorem (no axiom system proves all of the interesting facts about the integers), then modify that into a proof of the second incompleteness theorem (that every logic which proves its own consistency must be inconsistent). But it goes way further than that to Rice's theorem: every nontrivial semantic property of a computer program is undecidable. Put another way, the only way for the compiler to know that something is true is for there to be a really simple up-front convention which makes it true. Suppose you want to make sure, statically, that you never dereference a null pointer. This says that the only way a compiler could ever be strong enough to prove this is if it's syntactically impossible to create a null pointer in the language in the first place, so that it's a "trivial property" of all programs that they never dereference null pointers. Suppose you want to prove that a certain block of code is the fastest possible code which does a certain thing. The only ways to do this require the language to "normalize" all of its expressions so that there is only one block of code for everything you want to do. If there's more than one way to do it, then the analysis "is this the fastest code?" is nontrivial and you can't prove it! (You can always get heuristics of course to try to cover the most common cases, but your heuristics will never cover everything you want.) Suppose Microsoft wants to fix Word and Excel's macro systems to a new form that cannot contain viruses: the only way to do that is if the macro system is either (a) Turing-incomplete, so that you can analyze its programs, or else (b) unable to do the virusy things that you're worried about in the first place. Otherwise there will always be a macro-virus which passes the virus-checker.

skybrian 10y ago
In theory, sure. In practice, a program that takes a century to run is indistinguishable from a non-terminating program. If you prove a macro is safe by trying every possible combination then it could very well take that long. And we usually don't wait that long. A function that executes when loading a web page times out in the order of seconds. Once you have deadlines, all bets are off - the function is not deterministic for any large enough input. Equational reasoning does not preserve performance - it could cause a program that previously ran fast enough to time out. So, knowing that function terminates seems only theoretically useful. It doesn't tell us whether a program change is really safe. It would be more useful to put some kind of bound on the resources a function can consume. In Etherium's language, there is a concept of "gas" which is an abstract limit on how much work a function can do. (The advantage over a timeout is that it's not machine-specific.) I sometimes wonder if anyone has applied this concept to functional programming? Could we define a language so that it uses static analysis to maintain guarantees about a function's use of gas?