I suppose I’ll be the first person to point out that ECMAScript is fun and that “JavaScript functions” are not quite functions. Recall that positive infinity is spelled 1/0, and note that fac() doesn’t halt on at least one input:
>> function fac(n) { return (n <= 0) ? 1 : n * fac(n - 1); }
>> fac(1/0)
This is fine; we just have to keep in mind that ECMAScript’s numbers are not the natural numbers.
This lesson was great! Thanks for your hard work and attention to detail; this entire series has been delightful.
Thanks for being that person :) You’re right, of course. It also doesn’t halt on NaN, for the same reasons, and actually the problems start sooner than infinity – specifically at Number.MAX_SAFE_INTEGER. Why did I choose to use JavaScript to demonstrate formal verification …
… Also, thank you for the compliment - I hope you don’t mind, I added it to the course homepage!
Huh, I wouldn’t say they’re not quite functions - the domain is just a different set in this case (numbers + infinity element vs numbers). The proof by induction relies on the recursive call having a “smaller” element, and (1/0-1) violates that, so it doesn’t hold in this case.
Sure, you’re right. The proof also relies on the idea that subtraction by one is sufficient to access a predecessor, which isn’t the case in IEEE 754:
>> 1e20 - 1 === 1e20
Again, it’s not a big deal, but it’s important to keep in mind that we typically don’t have our desired natural numbers when working in popular programming languages.
the computing/programming terminology is different to the mathematical terminology.
in a programming context ‘function’ is used to describe a ‘procedure’, e.g. we call them functions in C. You can probably tell that I prefer the term procedure. Which I consider more correct.
Well, yes, I suppose I was being imprecise myself. I was referring to functions that don’t mutate global state, like the one in the parent comment’s code snippet (unless you want to argue that memory consumption / execution makes these not pure functions in the mathematical sense anyway, but that doesn’t seem pragmatic – no function executed by a computer would be pure by that definition). As for nontermination, it’s sufficient to extend the “range” with a “bottom” element and suddenly nontermination is still pure.
function add(x, y) {
globalCount += 1; // not part of the input
return x + y;
}
Or, maybe a way of putting it that we all can agree on is that they could be functions if we agree that the global state of the program is an implicit argument and return value to all function definitions. This makes proofs about them almost impossible without introducing frame conditions or using separation logic.
Frame conditions are what subset of the global state a function operates on, stated explicitly. Separation logic is similar, but allows you to ignore parts of the state that your function doesn’t modify a little more easily.
That’s a lot of extra machinery, just to treat something with a keyword of function as an actual function. You can see how it’s actually not a great name in retrospect, but it’s a little too late for that now. This isn’t unique to JS btw, this is all functions in all programming languages (yes including Haskell).
Right, like I mention in a sibling comment, I was still talking about functions in JavaScript that are written in the “pure” style. I was not suggesting an implicit state monad (“take the program state as argument”) / IO monad or anything like that. You can use regular old induction to reason about pure functions written in JS (and they have the advantage of being written in a language familiar to most readers), but you do have to be conscious of the differences Corbin points out (like the fact that JS nats aren’t nats!)
I don’t think I’d include the Ackermann function example in an intro to proofs about programs. I think that topic is foreign enough to most people that simple examples are sufficiently mind-expanding. In practice, I haven’t encountered many functions with similar characteristics to the Ackermann function. It’s basically the equivalent of a chess puzzle, meant to prove a point via some overindulgent setup.
Other than that, I love the topic, love the format, love the post.
I suppose I’ll be the first person to point out that ECMAScript is fun and that “JavaScript functions” are not quite functions. Recall that positive infinity is spelled
1/0, and note thatfac()doesn’t halt on at least one input:This is fine; we just have to keep in mind that ECMAScript’s numbers are not the natural numbers.
This lesson was great! Thanks for your hard work and attention to detail; this entire series has been delightful.
Thanks for being that person :) You’re right, of course. It also doesn’t halt on
NaN, for the same reasons, and actually the problems start sooner than infinity – specifically at Number.MAX_SAFE_INTEGER. Why did I choose to use JavaScript to demonstrate formal verification …… Also, thank you for the compliment - I hope you don’t mind, I added it to the course homepage!
Huh, I wouldn’t say they’re not quite functions - the domain is just a different set in this case (numbers + infinity element vs numbers). The proof by induction relies on the recursive call having a “smaller” element, and (1/0-1) violates that, so it doesn’t hold in this case.
Sure, you’re right. The proof also relies on the idea that subtraction by one is sufficient to access a predecessor, which isn’t the case in IEEE 754:
Again, it’s not a big deal, but it’s important to keep in mind that we typically don’t have our desired natural numbers when working in popular programming languages.
they aren’t pure functions because they can mutate state.
they aren’t total functions because they may not all terminate on all inputs.
they are procedures
We should stop saying “pure functions.” There’s no such thing as an impure function.
the computing/programming terminology is different to the mathematical terminology.
in a programming context ‘function’ is used to describe a ‘procedure’, e.g. we call them functions in C. You can probably tell that I prefer the term procedure. Which I consider more correct.
the qualifier is used for clarification.
Well, yes, I suppose I was being imprecise myself. I was referring to functions that don’t mutate global state, like the one in the parent comment’s code snippet (unless you want to argue that memory consumption / execution makes these not pure functions in the mathematical sense anyway, but that doesn’t seem pragmatic – no function executed by a computer would be pure by that definition). As for nontermination, it’s sufficient to extend the “range” with a “bottom” element and suddenly nontermination is still pure.
They aren’t functions:
Or, maybe a way of putting it that we all can agree on is that they could be functions if we agree that the global state of the program is an implicit argument and return value to all function definitions. This makes proofs about them almost impossible without introducing frame conditions or using separation logic.
Frame conditions are what subset of the global state a function operates on, stated explicitly. Separation logic is similar, but allows you to ignore parts of the state that your function doesn’t modify a little more easily.
That’s a lot of extra machinery, just to treat something with a keyword of
functionas an actual function. You can see how it’s actually not a great name in retrospect, but it’s a little too late for that now. This isn’t unique to JS btw, this is all functions in all programming languages (yes including Haskell).Right, like I mention in a sibling comment, I was still talking about functions in JavaScript that are written in the “pure” style. I was not suggesting an implicit state monad (“take the program state as argument”) / IO monad or anything like that. You can use regular old induction to reason about pure functions written in JS (and they have the advantage of being written in a language familiar to most readers), but you do have to be conscious of the differences Corbin points out (like the fact that JS nats aren’t nats!)
I don’t think I’d include the Ackermann function example in an intro to proofs about programs. I think that topic is foreign enough to most people that simple examples are sufficiently mind-expanding. In practice, I haven’t encountered many functions with similar characteristics to the Ackermann function. It’s basically the equivalent of a chess puzzle, meant to prove a point via some overindulgent setup.
Other than that, I love the topic, love the format, love the post.