Lambda the Ultimate

C.T. has been mentioned on LtU before. I do hope that it gets ever wider attention. I like this paper in that the approach is not mainly about making people be able to be programmers. It is about making people be able to understand things e.g. so they can (as I see it) understand items in the news, or talk about things over coffee. Even people who learn to program often miss the forest for the trees, I think.

How Computers Work: Computational Thinking for Everyone

What would you teach if you had only one course to help students grasp the essence of computation
and perhaps inspire a few of them to make computing a subject of further study? Assume they have
the standard college prep background. This would include basic algebra, but not necessarily more
advanced mathematics. They would have written a few term papers, but would not have written
computer programs. They could surf and twitter, but could not exclusive-or and nand. What about
computers would interest them or help them place their experience in context? This paper provides
one possible answer to this question by discussing a course that has completed its second iteration.
Grounded in classical logic, elucidated in digital circuits and computer software, it expands into
areas such as CPU components and massive databases. The course has succeeded in garnering the
enthusiastic attention of students with a broad range of interests, exercising their problem solving
skills, and introducing them to computational thinking.

"The course includes some computer programming, but does not dwell on it."

I wish more real-world day-job programmers (including refreshing my own self I can't be too hypocritical) really learned these things:

The big ideas in the honors course are
1. the correspondence between digital circuits and formulas in logic,
2. how abstractions facilitate combining solutions to small problems to form solutions to big ones,
3. how algebraic formulas can specify computations,
4. how models expressed in software capture the behavior of processes and devices,
5. how important, complex algorithms derive from simple, definitional properties,
6. how different definitional properties can produce the same results at vastly different computational
expense,
7. how computational expense makes some useful devices feasible and renders others infeasible,
8. and how all of these ideas bear on the ability of computers to deal with information on the massive
scale needed to provide services like search engines, internet storefronts, and social networks

Equivalence of functions is, in general, undecidable. But specific instances of it are usually decidable. Equivalence can be proven via structure analysis, or disproven via structure analysis or by example. Equality can be proven on functions whose input is limited to a finite set simply by exhaustive testing of all possible inputs. So, while it's true that there will always be an infinite set of pairs of functions for which we cannot prove equivalence or nonequivalence, it isn't really the case that we can't ever prove anything.

But what notion of 'equivalence' is useful?

What if we have two functions that are provably equivalent where their results are defined, but result in errors in different cases, or result in *different* errors in some cases? If I can prove, in the context of a particular program, that no possible call to a function will be a member of either error-causing set, then the functions are equivalent ... for purposes of that program. ie, they are observationally equivalent for the particular subset of valid inputs that we're interested in.

What if we have two functions that do equivalent things to members of slightly different types? For example, if I have two string-concatenation functions, but one of them concatenates a string class on which fifteen other operations are defined and one of them concatenates a string class on which thirteen of the _same_ other operations and three _different_ other operations are defined? These concatenation functions are not exactly mathematically equivalent, but in some very important way they are exactly the same, and may even be expressed by exactly the same source code. If a mathematician said these functions weren't equivalent, as an engineer I would roll my eyes and ignore him. If my job required me to satisfy his useless notion of equivalence, I would *make* the functions equivalent by just defining the 'missing' operations in both classes.

What about having 'equivalent' multiplication functions on, say, ints and rationals? If I posit that there is a multiplication function on a 'number' type that both of the other functions are subsets of (that is, they give equal results on equal inputs, for all inputs they can be given), is that a useful notion of equivalence?

What if we have two functions that return exactly the same results in all cases, and we can prove it ... but one of them takes N-squared memory and NlogN runtime, and the other takes N-squared runtime and NlogN memory? As an engineer I'd find this semantic equivalence and resource-requirement nonequivalence useful and swap one for the other depending on whether speed or memory use were more important. As a mathematician, I don't even know whether I'd be working with a notion of equivalence that would note the difference.

In the end, 'equivalence' is any relation that's transitive, symmetric, and reflexive. There's an infinite number of choices of such relations, and people who talk about function equivalence often do so without saying which equivalence they mean. Or, importantly, which equivalence is most useful in some relevant context.

And while you're chewing on the question of what 'equivalence' is most useful in a given context, what notion of proof is most useful to establish it?

What if we have a pair of functions which has been observed to return the same answer for the same inputs on a randomly-selected billion possible inputs ... and monitoring both has revealed that we have achieved 100% code coverage in both functions while doing so ... and other monitoring, plus a few million not-so-randomly-selected inputs, has assured that all possible combinations of taken and not-taken conditional branches in both functions have been exercised, on inputs that differ from each other by the theoretical minimum possible for that input type? As a mathematician, I couldn't claim that I know these functions are equivalent. As an engineer, I'd consider the indications of function equality to be strong enough that I wouldn't mind the absence of a proof. I'd feel comfortable swapping one for the other, especially if they are both relatively short.

Why short? Shortness limits the possible semantic complexity to some wobbly notion of a boundary, making it less likely that one or both contains subtleties not revealed by the extended fuzz-test. If one or both of the functions were twice as long, I'd want more fuzz-testing before I'd feel as comfortable swapping them. This corresponds to some intuition about reaching a particular certainty level, but that certainty level, no matter how you slice it, is less than an absolute proof.

So, here's a question. Is it useful for programmers to go with some 'heuristic' of function equality, or an engineering-grade 'indication' of function equality, if no mathematically certain proof is available and by doing so they can achieve measurably better results? Is it worthwhile for PL theorists and researchers to seek and refine such 'heuristics' and ways of estimating the strength of such 'indications' (rather than 'proofs') of function equality?

In mechanical engineering, strength of materials is always an estimate. In programming, sometimes the strength of our knowledge is also an estimate. This is a problem, but not necessarily a disaster, in terms of producing useful results. Mechanical engineers compensate by including a 'safety margin' well beyond the requirements of the particular job. How should programmers compensate?