After nearly a month of being tortured by Coq, I have finally, finally finished Logic Foundations. As the lead title of the Software Foundations series, it really is something. Here I just want to share some deeper understanding I’ve gained of two concepts: symbols and interpretation. The main text has almost nothing to do with programming itself.
Preface
I’m not going to summarize what the book teaches. Instead, I’d like to muse a little about two important concepts I kept running into while reading it: symbols and interpretation.
First, a quick intro to Coq. Put simply, it’s a functional programming language. The weird part is that it can also be used as a proof assistant. Some of my projects required Coq (and, sure, I was curious about it too), so I started with a document called Coq in a Hurry. It was of absolutely no use: it did not help me learn Coq in a hurry. And so I set off down the broad narrow highway goat track that is Software Foundations.
When I first saw the title I just laughed. Software Foundations? How foundational can it be? And the first volume is literally called Logic Foundations. LOL, it’s just an intro book, I’ll have it mastered in no time, right? Then, slowly, I came to understand everything: in PL, anything that calls itself “foundations” is lying to you. At Penn the course is numbered CS500, which means it’s meant for grad students and the very best undergrads. Of course, by the time I realized all this, I’d already been lured aboard the pirate ship.
Anyway, it’s still a really good book, because it’s refreshingly sane. It seems to get updated before every offering of the course, which means the material still works on the latest stable Coq. Unlike certain cursed textbooks that, despite being published in 2021, insist on using their own homemade software that stopped being supported N years ago (and only runs on Windows). Yes, I’m talking about you, Thinking Programs! The book itself is pretty good, but the code is hopelessly dated: fossilized code running on heirloom software, and extremely unfriendly to the command line and to Macs.
Many thanks to the authors of SF for making it publicly accessible, so that all of humanity can learn from it freely.
Symbols
As a small child, I often wondered: what exactly is “我” (Chinese for “I”)? I don’t mean this in any philosophical sense. Swap “我” for any other word and the nature of the question doesn’t change: what exactly is “红色” (“red”)? Or what exactly is “dASYg”?
The clever kids among you may have noticed already that the 【things】 wrapped in quotation marks here are simply symbols, which may carry no meaning at all. But then the question gets really strange: why is the symbol “我” able to express the meaning of 【myself】? Did someone first assign the meaning 【me】 to “我”? Does every Chinese speaker understand that “我” stands for 【me】? These big questions dealt a huge blow to my young heart, and it wasn’t until I learned that there’s a special kind of human called the color-blind that I slowly began to get it.
In their eyes (more specifically, red-green color-blind eyes), “红色” doesn’t mean the 【red】 I see. And for people who can’t read Chinese characters, “红色” can’t even convey the meaning of 【red】 at all. At best it’s a symbol. They might not even be able to tell whether it’s one symbol or two. In fact, symbols may simply be different in different people’s eyes. And all the text here is nothing but a pile of symbols stacked together; I’m honestly grateful that “you”, looking at this pile, can guess what I’m trying to say.
Formally
Let me start with a Wikipedia link on formal symbols. “Formal” gets translated into Chinese as 形式化, literally “made into form”, and for a long time I never really understood what the word meant, but now it’s slowly clicking. A formal symbol is a symbol stripped of meaning: all that matters is what the symbol looks like. It’s basically the opposite of the idiom 得意忘形, which literally reads “grasp the meaning, forget the form” (though in everyday Chinese it actually means getting so pleased with yourself that you lose your composure).
In the pursuit of formalization, many textbooks bring up language. This is the most interesting part: linguistics, computer science, mathematics, and even philosophy all meet in this weird little place! If formal symbols want to form a sentence (that is, combine into more complex symbols), they have to rely on a grammar (formal grammar). This grammar is no different from the grammar we learned in foreign-language class as kids: a set of rewriting rules for symbols. Take the simplest subject-verb-object sentence in English: each of subject, verb, and object (symbols) can be rewritten into another suitable symbol, producing another concrete sentence.
Mathematical logic also leans heavily on symbols. Logical deduction can be seen, on the one hand, as a relation between semantics (meanings), and on the other, as pure rule-based symbol manipulation (Sequent calculus). And if you dig any deeper, you end up in philosophy. There’s a branch called 【形而上学】 (metaphysics; literally “the study of what is above form”) that has quite a bit to do with symbols and logic. Since I don’t actually understand it, I won’t ramble about it here. But I do think the Chinese word is ambiguous. How should you read the “而上” (“and above”) part? As 【built on top of XXX】, or as 【another realm beyond XXX】? The English is Metaphysics, and I lean toward the latter.
Let me wrap up this section with “1 + 1 = 2”. Ever since second grade I never understood why this equation holds. But before asking why one plus one equals two, maybe the question more worth asking is: why does “1” stand for 【one】?
Interpretation
Simply put, interpretation is assigning meaning to symbols (wiki). So when I ask why “XXX” stands for the meaning 【XXX】, perhaps the most reasonable answer is: we assigned the meaning 【XXX】 to the symbol “XXX” itself. Back to the earlier example: “1” meaning 【one】 and “2” meaning 【two】 are, at bottom, just people representing meanings with symbols for convenience. The same meaning can be represented by different symbols, and the same symbol can mean different things under different interpretations. Roman and Arabic numerals use different symbols, yet numbers of equal value mean the same thing; meanwhile the symbol “艹” means different things in Chinese and in Japanese (lol), i.e., it has two different interpretations. Worth noting: the “(lol)” I just wrote doesn’t mean I actually laughed. It’s there because “艹” (in Chinese, a euphemism for a certain four-letter word) is used in Japanese internet slang to mean 【lol】. Ambiguity really is everywhere.
Humans can never truly understand one another.
In formal logic, interpretation isn’t necessary, but humans probably need some kind of interpretation. This line now resonates with me more deeply than ever. How do you know that the “thing” someone expresses with symbols is the same “thing” as their own interpretation of those symbols in their head? Language often feels a bit feeble. For one, it can’t always express a person’s real thoughts precisely, and there’s no guarantee the receiver will understand it the way it was meant. Thinking this through, I suddenly grasped why the Trisolarans are a superior species: they can perceive what’s in each other’s minds, and that kind of expression, free of language, conveys meaning far more precisely. I also understood why the Tower of Babel could never be built: if people can’t even share a language, mutual understanding is a fantasy.
Stupid Machines
Long ago, when I first came across the phrase “graphing calculator”, I thought it was an incredibly cool concept. One of its features was “symbolic computation”. That phrase dealt an even bigger blow to the heart of the human cub I was back then: what on earth is symbolic computation? I couldn’t wrap my head around it for ages; I needed an 【interpretation】. Aren’t plus, minus, times, and divide symbols? What are the “symbols” here, then? Later I slowly came to understand everything. Simply put, it’s the counterpart of numerical computation: you can mix symbols (e.g., X, Y, Z) into your calculations. Simplifying polynomials with symbols in them requires exactly this ability.
Computers are dumb. They only know 0 and 1.
Someone told me this when I was young. At first I didn’t get it, because computers could display text and paragraphs in all kinds of languages, do all kinds of calculations, even “understand” what I wanted them to do. But thinking about it now, maybe there’s something to it. That text and those calculations aren’t understood by the machine; they’re just displayed (printed) as symbols, one after another. The ones who really interpret the meaning behind these symbols are humans, not computers, and all the machines truly 【understand】 are 0s and 1s. Then again, if humans can’t understand one another, can humans understand computers? How would humans even know that computers can’t understand the meaning of these symbols? Maybe only the people who actually design the chips get a say; the rest of us just know that this black box produces content we can 【understand】.
In computing, the big limitation of neural networks is usually said to be that they’re 【uninterpretable】. Although some methods for explaining them have been developed, this still seems to be a major headache for researchers. If people can’t understand what some blob of a model is actually thinking, why should they trust it to produce results that are correct enough? After we feed a machine huge amounts of data (symbols), it can learn the rules of inference among those symbols. Yet we can’t understand why it spits out certain bizarre symbols, and the machine itself doesn’t understand what those symbols mean either. So maybe machines need an interpretation too. On the day machines can truly 【interpret】, perhaps the 【computer】 will be more than just a “computer”.
Epilogue
Then again, why do we think we 【understand】 symbols at all? Could it be that the human brain simply replaces these symbols with more complex ones (a low level representation), and we just act on them according to certain rules after processing? (lol)