Some notes about J from today
Charting
chart =. {{ l {~ >. (<: #l =. u: 16b20, 16b2581 + i.8) * y % >./ y }}
] dat =. 10 ? 20
13 18 9 0 1 4 16 19 3 7
chart dat
▆█▄ ▁▂▇█▂▃tsvector in J
A tsvector in Postgres is the tokens of the input and their locations. We can compute this in J by cutting the input and associating it with the number of words of the input. Here is the Postgres example:
SELECT to_tsvector('english', 'a fat cat sat on a mat - it ate a fat rats');
to_tsvector
-----------------------------------------------------
'ate':9 'cat':3 'fat':2,11 'mat':7 'rat':12 'sat':4In J:
txt =. 'a fat cat sat on a mat - it ate a fat rats'
w ([,<@])/.. i. #(w =. ;: txt)
┌────┬──────┐
│a │0 5 10│
├────┼──────┤
│fat │1 11 │
├────┼──────┤
│cat │2 │
├────┼──────┤
│sat │3 │
├────┼──────┤
│on │4 │
├────┼──────┤
│mat │6 │
├────┼──────┤
│- │7 │
├────┼──────┤
│it │8 │
├────┼──────┤
│ate │9 │
├────┼──────┤
│rats│12 │
└────┴──────┘There are some differences due to cleanup that Postgres does on the input which I’m not doing. But the idea is pretty much the same.
Collecting Data using /..
Considering the following:
]data =: _2 ]\ 'Fred';90;'John';75;'Fred';95;'John';85;'Susan';100;'John';86
┌─────┬───┐
│Fred │90 │
├─────┼───┤
│John │75 │
├─────┼───┤
│Fred │95 │
├─────┼───┤
│John │85 │
├─────┼───┤
│Susan│100│
├─────┼───┤
│John │86 │
└─────┴───┘The documentation provides the following solution:
]s =: ({."1 data) <@;/. ({:"1 data) NB. Use first column as keys; collect second-column values
┌─────┬────────┬───┐
│90 95│75 85 86│100│
└─────┴────────┴───┘
(~. {."1 data) ,. s NB. Reinstall the name
┌─────┬────────┐
│Fred │90 95 │
├─────┼────────┤
│John │75 85 86│
├─────┼────────┤
│Susan│100 │
└─────┴────────┘I found my own solution:
(}:"1 data) ([,<@;@])/.. ({:"1 data)
┌─────┬────────┐
│Fred │90 95 │
├─────┼────────┤
│John │75 85 86│
├─────┼────────┤
│Susan│100 │
└─────┴────────┘The channel found this:
(,<@;)/../|:data
┌─────┬────────┐
│Fred │90 95 │
├─────┼────────┤
│John │75 85 86│
├─────┼────────┤
│Susan│100 │
└─────┴────────┘This notices that we have one column on the left and one on the right and inserts the calculation between them, reducing the amount of tearing apart we have to do by hand.
(}:"1 (,<@;)/.. {:"1)This is a tacit definition from someone else on the channel, which reduces parens by using a tacit definition.
My dad used WordPerfect 5.1 for DOS to manage our tape library.
The first computer I really had regular access to was my parents’ 486DX 33 MHz with 8 MB of RAM and a 250 MB disk. It came from the shop with various software, I don’t know if that included WordPerfect 5.1 for DOS or not. I don’t know if the shop bundled it—this was common in that era, but my parents friend Jim “Computer Man” Myers (recently deceased) also came and brought shareware over to the house and might have snuck in a copy. It was a widely pirated program.
My parents love poetry, although now that my father has dementia I doubt he appreciates it much. He suffered a traumatic brain injury when he was around 18 that left him with Broca’s aphasia, which meant for him that while he could understand people without much trouble, it was hard to string a complete sentence together. We got used to slipping him a word he was groping around for so he could finish his utterances. He used to write poetry too. One was published in Arizona Highways although I can’t find a link to his poem online.
I think trying to figure out how to use this machine led him to take a community college class on computer literacy. Whoever taught the class must have been a complete maniac because the text was The Secret Guide to Computers, I believe 16th edition or so. If you haven’t seen this book, you are really missing out, because it’s enormous, loaded with tacky clipart, and has the author’s opinion on pretty much everything related to computers over the last decades. The author, Russ Walter, has his phone number on the cover and says you can call him if you ever have troubles.
I did have troubles at one point, I had made the mistake of using Drivespace^3 on another computer and lost all my data. I called Russ and he basically said that program is crap, hope you have backups. I felt let down by this at the time but of course he was right.
I stole this book from my dad and learned an enormous amount from it and I think it led me to my early obsession with programming language diversity.
What did my dad do with this computer? Much less than my mother, who used it to type up all sorts of work-related stuff. She used WordPerfect to write memos and training materials, and she used Print Shop Pro to make certificates and other stuff for work. We used something like Greeting Card Creator to make cards for special occasions. But my dad apparently did two things with it: he wrote up his personal journal and poetry, and he maintained the tape library.
My mother is a bit of a hoarder and my dad was a bit of a financial worrier. My folks did some odd things at the intersection of hoarding and penny pinching. One was the tape library. We must have arrived fairly early on to the whole VCR scene; I have a fairly early memory of trying to watch Zebra in the Kitchen by finding the tape in the list. The list looked something like this:
Buckaroo Banzai......................93, 204
Robin Hood...............................123The movies were alphabetically sorted, and if there was more than one number it meant that the movie had been recorded twice. We had basic cable and sometimes got HBO or Cinemax during a free week or something. Mom would buy extra tapes for when that would happen. The VCR was set to the lowest quality setting so she could cram 6 hours of video onto one tape. She’d pop the tape out, put the label on it and list the movies that were recorded on it and then give it to Dad. He would figure out the last number in the library and write the new number on the tape and go off to the computer room and update the list by hand. I think we topped out around 350 tapes; my brother thinks 400, and they were stored in several bookcases around the house. Most tapes had 2 or 3 movies on them.
I recovered files from this computer some time ago but they’re sitting on another computer right now that I don’t have access to. I started copying the files onto my Dropbox so I could go through them but the upload got stalled out after 6 hours or so. Still I have seen enough other samples of his documents to be fairly sure that he organized this file without using either the built-in sort function or right-aligned tabs or dot leaders. I recorded a session of myself pretending to do this with WordPerfect 5.1 in DOSBox, but using those features:
You can probably tell from this description that what my father really needed was a desktop database. As far as I can tell, he didn’t really survive the transition from DOS to Windows. He eventually became somewhat conversant with the Mac, able to do the same kinds of things he did in DOS, but Windows was I think a bit too much for him at the time. I think the situation with my mom was the opposite; DOS was really befuddling but Windows (and eventually Mac OS X) were pretty easy to get around. Neither one of them ever really became users of desktop databases like Access. I think dBASE would have been way too much for him, although if he’d never had that brain injury I’m sure he would have loved it.
WordPerfect is kind of an amazing program. You can learn the fascinating history by reading this excellent book Almost Perfect but it raised for me the question of “what is a word processor?” The answer, in brief, starts out with the Wang 1200 as “a typewriter with memory.” WordPerfect started here and evolved in many interesting directions. Apart from the somewhat obvious functions you see in the above recording, it has an interesting “math mode” that deserves a longer post of its own, which doesn’t really exist in modern word processors.
Some famous writers still use DOS word processors like WordPerfect and WordStar. A part of me assumed that this was because of the “distraction-free” nature of these programs; another author made similar investigations. Doing my own learning, I can see some truth to that, and that running WordPerfect in an emulator doesn’t quite do it justice because you can just pop over to your browser and get distracted. But another way it doesn’t quite work is that every function key does something in WordPerfect. To get access to everything it can do you would have to eliminate all of DOSBox’s key bindings. WordPerfect came with a “template” you put over your amazing Model M keyboard’s function keys to see at a glance what it could do. You can see it at Xah Lee’s site. I imagine using WordPerfect 5.1 for DOS as an expert user, you would be able to do things extremely quickly. It was a very high-bandwidth conversation between the user and the machine. Not for my parents, of course, but for expert users.
For my parents, it was just a great way to write a professional letter, a personal journal, a poem, or to manage the tape list.
I finished Lockhart’s Lament, the 25-page version, and I have some feedback about it.
On Proof
I regard proof as being the defining activity of math. Really the trio of axiom-theorem-proof. However, proof is the real heart of the matter.
I used to have a sort of mystical admiration for the idea of proof. Then Tyler taught me a little bit about Coq, the theorem prover, using Software Foundations. I learned that proof is always intended for an audience, and that the most objective audience would obviously be a computer, a program that is going to make the same determinations every time, thus formal proof is the best kind of proof. Tyler didn’t say this, but it was one of my takeaways anyway.
Now taking Basic Concepts of Mathematics, I’m seeing proof as a story. The audience may vary—I’m a weaker audience than my professor, so I need more hand-holding. But an informal proof can still be rigorous. And I think this is the point that Lockhart is making about teaching kids to prove: we should not hold them to the same standards of rigor, but we should nonetheless expect them to make a mathematical argument.
This reminds me of the “black box game” which I learned about, as a way to teach your kids something about functions. The way you play the game is they give you a number and you give them another number, and they have to figure out how you came up with it. For instance, if you give me 3, I might give you 3, and if you give me 4, I might give you 5. If they know about odd numbers, they may say, “oh you’re giving me an odd number, either my number or the next odd number.” This is a way of helping kids think about functions without being too limiting about how they are constructed. (Another key takeaway for me from this class was that a function is not a bunch of algebra, it is defined if there is a way to find the unique value associated with the argument, whether that is a bunch of algebra or not.)
On Math and Science
Tyler provides an interesting definition here: math is about deduction and science is about induction. In science, we chip away at irrelevant details of reality to try and generalize to everywhere. In math, we can never depart the realm of pure reasoning and make contact with actual reality. I find this thought quite beautiful. It’s almost like a limit, defined from the left and the right, but there’s no reaching the limit other than by assuming it. A beautiful thought, I guess, to me, apropos of nothing in particular.
On Education
Lockhart returns repeatedly to a metaphor of a music teacher who is unable to play an instrument or has never heard music but is simply able to manipulate the notation. There’s an allure to this metaphor so I can’t completely begrudge him but I do have some feedback here.
First, school can and often does have negative effects in every subject. I actually think you can point to music as an example of this: Benn Jordan recently did a video about why there are so few women in the music industry and one (of many) reasons is that we typically make girls learn symphonic instruments like violin and cello, whereas we allow boys to learn instruments like guitar and drums—which are actually used in the modern music industry. The folks with bumper stickers bemoaning funding for band class in school are of course not imagining that we’re going to fill the room with 808 clones and electric guitars with distortion pedals and allowing real noise to be made. They’re picturing 30 kids playing a chamber music piece written sometime between the invention of the printing press and the electric lightbulb to a room full of well-dressed parents calmly golf-clapping. Every subject is ruined by school, not just math. Hence the joke about those who can and those who teach. My apologies to a certain reader who absolutely can is about to start to teach.
That said, I think the curriculum is changing, albeit not to the extent that Lockhart would like. But this essay is 20 years old now—some sympathizers have had time to get power. My kids love their math classes—they’re in 4th and 1st grade—and one of them said her entire class asked for more math homework. They’re worksheets, sure, but they like now to show you a half-dozen ways of solving similar problems. My son clearly has multiplication tables memorized, but at no point did the school send him home with flash cards and tables to fill out. I don’t know exactly how he learned it, but he knows the material. Things are not the same as when I was a kid.
You can actually see the effect of this in places like National Review. We have here a great example of people demanding that things be different, and then being upset when they are not the same (which is exactly what you expect from National Review). But in fact, I recognize some of these problems and several of them are great—if you’ve been taught the material. But many of these problems are using new approaches and if you weren’t taught them and aren’t inventive enough to figure them out, well, you see what happens.
In Conclusion
I had a powerful experience taking this class, and reading “A Mathematician’s Lament” while taking it helped me acknowledge that it is a powerful experience. Lockhart wants my kids to have that experience too. This isn’t a coherent vision of how to restructure math education. It’s a plea for people to experience math the way they experience art. I’m sad that I was 39 before this happened to me.
I want my kids to experience this too. Preferably before they turn 39.
I recently became aware of continued fractions, because my friend Randy mentioned that they are a representation of some insane thing in topology that he mentioned offhandedly and which sort of made sense while he was talking but I really could not reconstruct. However, continued fractions are interesting in their own right, and I started working on this post before I saw the Mathologer video on this topic.
A continued fraction is a nightmare scenario where the denominator of a fraction contains another fraction, whose denominator contains another fraction, and so on, perhaps forever. We can calculate a continued fraction by repeatedly taking the inverse of a value and adding a constant. This may seem counterintuitive at first, but since the denominator of a denominator is in the numerator, it makes a weird kind of sense that you can just keep on inverting. For instance, the Golden Ratio can be calculated by starting with 1 and then in a loop, adding 1 and inverting. Such an expression will eventually converge to the best floating point approximation, and that calculation looks quite trivial in J and APL:
((1+%)^:_) 1
1.61803Similarly in APL:
(1+÷)⍣=1
1.618033989Tyler did mention that I would of course resort to these languages as some kind of humble brag. Which is true and fair. Expect it to get worse if I ever learn linear algebra.
Both of these expressions essentially construct an “add one and invert” function, which they then locate the fixed point of, given an input of one. The choice of input doesn’t really matter much:
(1+÷)⍣=100
1.618033989
(1+÷)⍣=0.1
1.618033989This turns out to be a stock example in the Dyalog documentation:
1 +∘÷⍣= 1 ⍝ fixpoint: golden mean
1.618033989Furthermore, it turns out every square root can be expressed in a similar way too, either by a finite or an infinite repeating continued fraction. The trick is discovering what the base number is and what the repeating number is. For instance, for 2, the base is 1 and the repeating digit is 2:
1+÷((2+÷)⍣=2)
1.414213562
(1+÷((2+÷)⍣=2))*2
2Similarly, for 5, the base number is 2 and the repeating digit is 4:
2+÷((4+÷)⍣=1)
2.236067977
(2+÷((4+÷)⍣=1))*2
5These same calculations can be made in Haskell if we develop our own fixpoint. We can generate this with iterate but we need to determine when to quit with something like this:
untilEqual :: (Eq a) -> [a] -> a
untilEqual (x:y:xs) | x == y = x
untilEqual (x:y:xs) | otherwise = untilEqual (y:xs)Now we can create somewhat more readable versions of these things:
*Main> untilEqual $ iterate (\x -> 1 + 1 / x) 1
1.618033988749895
*Main> 1 + 1 / (untilEqual $ iterate (\x -> 2 + 1 / x) 1)
1.4142135623730951Let’s make this a helper function.
squareRootCf :: (Fractional a, Eq a) => a -> a -> a
squareRootCf a b = a + 1 / (untilEqual $ iterate (\x -> b + 1 / x) a)Now we can compute these more easily if we know the basis and repeating digits:
*Main> squareRootCf 1 2 -- sqrt 2
1.4142135623730951
*Main> (squareRootCf 2 4) -- sqrt 5
2.23606797749979
*Main> *(squareRootCf 3 6) -- sqrt 10
3.1622776601683795It turns out Haskell has a rational type we can use, in Data.Ratio:
infiniteCf :: (Integral a) => a -> a -> [Ratio a]
infiniteCf a b = map ((a % 1) +) partials
where
partials = (1 % b) : [recip ((b % 1) + prev) | prev <- partials]We can then generate rational approximations:
*CFrac> take 10 $ infiniteCf 1 1
[2 % 1,3 % 2,5 % 3,8 % 5,13 % 8,21 % 13,34 % 21,55 % 34,89 % 55,144 % 89]As you can see that’s producing 2, 3/2, 5/3, 8/5, 13/8, etc. which is the Fibonacci-like sequence of ratios you get for approximating the Golden Ratio. This is kind of explained by the above Mathologer video, so to spoil it for you he calls this is the “most irrational number” because it has the slowest-to-converge repeating continued fraction.
We can also produce some pretty compelling root-2 approximations the same way:
*CFrac> take 10 $ infiniteCf 1 2
[3 % 2,7 % 5,17 % 12,41 % 29,99 % 70,239 % 169,577 % 408,1393 % 985,3363 % 2378,8119 % 5741]What’s interesting about this you ask? One thing I find interesting is that you aren’t really bound by what floating point happens to represent. You could of course resort to using some arbitrary precision library, but then you might want to know what’s (one way) of doing whatever it does under the hood. How do you get arbitrary precision? One way that you could build a system like that would be on continued fractions. But you don’t really get perfection out of a continued fraction representation of a square root. Instead, you get something back where you can say, I want more precision than that, and it will give you another, better rational approximation. For instance, we can ask Haskell to take the square root of two and tell us what its ratio is:
*CFrac> toRational $ sqrt 2
6369051672525773 % 4503599627370496Seems pretty good, but it doesn’t take us very many iterations to beat it:
*CFrac> length $ show $ denominator $ toRational $ sqrt 2
16
*CFrac> takeWhile (\x -> length (show (numerator x)) < 18) (infiniteCf 1 2)
[3 % 2,7 % 5,... 41 more elided..., 83922003724759193 % 59341817924539925]So we have already discovered that 83,922,003,724,759,193 / 59,341,817,924,539,925 is a better approximation of the square root of 2 than 6,369,051,672,525,773 % 4,503,599,627,370,496, which interestingly, does not appear in the list of rational approximations we generate—which would be very surprising, because the rational approximations generated by the continued fraction are proven to be the best rational approximations at their information content, except for a couple problems: namely, that floating point numbers are literally the worst, and we’re probably using some kind of hardware root approximation that is very fast and, you know, tolerably accurate (note that (sqrt 2)^2 = 2.0000000000000004, for instance).
Another fascinating property of continued fractional representations of these numbers is that they bounce back-and-forth above and below the value they’re approximating. So you could easily specify a precision you want, and just take from the representation until the difference between the last two approximations you generated is less than that precision. This is starting to sound suspiciously like a Dedekind cut (infinitely many better and better rational approximations of a real number), or maybe like the epsilon-delta concept of a limit (find me an approximation that’s closer than epsilon to the number).
It turns out this information isn’t very new; in fact Bill Gosper of Lisp/Macsyma fame developed a procedure for doing arbitrary sums and products with continued fractions. If you find that appendix hard to read, perhaps you’ll enjoy Mark Jason Dominus’s discussion of the same topic a little more, including a reference implementation of continued fractions in C.
I live in Socorro, New Mexico, which is near to the Alamo Navajo chapter. The Navajo are the largest Native American tribe by membership in the United States, and their combined lands are the largest of any tribe in the United States. Their reservation includes much of their historical homeland. Their language is the most widely spoken Native American language in the US—I often hear Navajo spoken at Walmart. Navajo culture is an important part of what makes New Mexico the special multicultural melting pot that it is.
I developed an interest in the Navajo language a couple years ago. The Navajo language seems practically engineered to differ from English on as many levels as possible:
- Tone and length distinctions
- A wealth of consonant sounds we either do not have or do not distinguish
- Zero noun morphology
- Verb morphology that makes linguists blush
- Animacy distinctions
- Productive dual number
It is rightly held in high esteem by linguists and is thoroughly different from any language a random American like me might be familiar with. Unlike many other Native American languages, there is also a huge amount of quality resources for the Navajo learner.
In general, I think spending money on Navajo language resources does more good than harm. Demand for Navajo language materials makes it more profitable to produce them. The Duolingo course is OK. If you have the money I have heard that the Rosetta course is very good. I bought several books, I particularly liked Conversational Navajo because it came with a CD. Navajo orthography and pronunciation is very regular, although it is difficult for adult second-language learners. I can’t roll my r’s very well, but that doesn’t matter in Navajo because there’s no rs. If you can imitate beatboxing you can make ejective consonants and you will be able to make the sounds. Unfortunately English treats aspiration as allophonic variation so there are some phonemic sounds in Navajo that you’ll have some trouble distinguishing. But you will be able to produce them.
If you want to know more about the grammar, The Navajo Language is pretty complete and goes into huge detail, but will be hard to learn from. The Navajo Verb is just amazing (I have skimmed it via ILL) but way beyond my level. The language is just about as far from English as you can get, and pretty irregular. At the moment I’m fairly content that I can say hello, what’s up, and distinguish it from other languages that are spoken nearby.
There are a lot of massive and wonderful Navajo books. If you want to learn Navajo and live outside New Mexico and Arizona, I would strongly recommend figuring out a way to get interlibrary loan going through your school or a local academic library, and start pulling stuff in from libraries here.
There’s also a lot of apps. You can listen to Navajo radio, you can get Clayton Long’s videos on Youtube if you have patience for it. There’s another guy, Daybreak Warrior who goes over words and you can listen to his stuff and really improve your pronunciation.
Navajo culture is really interesting and beautiful. I enjoyed what I got from Diné Bahane’ and there are lots of other booksto read as well, like Sharing the Skies and Food Sovereignty the Navajo Way. I would strongly recommend getting familiar with Navajo Taboos. There are a lot of things it really isn’t OK to ask about. You should expect to get a somewhat aloof treatment, at least until you make a friend. People love to tell you their story and you’ll be really surprised by what you hear, but don’t press anyone about superstitions or supernatural stuff.
When I started I had big dreams about becoming fluent. Contact with reality kind of disabused me of that notion. I’m content to be a friendly neighbor. But there’s a ton of resources out there, many of them free or inexpensive, and I don’t think you’re harming anyone by loving something enough to study it.
Originally posted on reddit but the original context is now gone.
I am just finishing up the book Math Without Numbers by Milo Beckman. This is a good book for a layperson like me, in that in introduces lots of interesting stuff and provides a kind of a map to mathematics.
I have a hunger for more knowledge about math, and I found the book a bit like an amuse-bouche before a meal that isn’t coming. I’m not entirely sure what to do about that, since I’m not prepared to return to school for math, yet I’m not satiated by superficial treatments of math from YouTube videos and the like. I think if I had taken an extra year or two of math in college, it would be easier for me to make progress on my own.
Real Numbers
I got interested in the real numbers a few years ago and read Essays on the Theory of Numbers by Dedekind, who has this amazing quote at the beginning of the book:
The present memoir soon after its appearance met with both favorable and unfavorable criticisms; indeed serious faults were charged against it. I have been unable to convince myself of the justice of these charges, and I now issue a new edition of the memoir, which for some time has been out of print, without change, adding only the following notes to the first preface.
The real numbers present a sort of confounding problem. We need real numbers to handle irrational numbers such as √2 and the like, which can be approximated. But the uncountability of the real numbers, their absolute continuity, is a property that is needed for calculus. Yet we’re unable to construct a single real number that doesn’t also belong to the set of algebraic numbers, which are countable. This is sometimes called the “hay in the haystack” problem. Neither one of us has ever seen a real number and probably never will.
Topology
Measure is an elementary topic of topology, and I’m an expert because I’m on page 35 of a book about it, Introduction to Topology. The book is great. On page 35, though, I got the answer to a question I sort of posed a number of years ago in A Heretical Calculus, why don’t we use a number system with an actual infinity and actual infinitessimals, since that’s what Newton did and for a few hundred years it seemed to be fine?
Figuring out a way to solve our problems with these “hyperreal” numbers occupied math for quite some time but the solution, the epsilon-delta definition of closeness, is not just a nice solution. It happens to open up the possibility of doing calculus to many other situations than just real numbered functions. Exercise 2.4 in Introduction to Topology has you prove that integration of functions over a fixed domain form, themselves, a metric space. This means you could in principle do anything you do with calculus over that space, like integrate.
Talking to my friend Mike Tamburro about it, I get the sense that topology is not so much about donuts and spheres and whatever as it is about questions like, what does it mean for points to be close? What is a neighborhood? What do does “connected” mean? All of these questions seem to spring forth from the idea of continuity. In our first-year calculus classes we get a very pragmatic sense of what continuity is about, but what does it really mean?
Proof
Solving the first three assignments on page 35 of the topology book, I found myself wrestling with the same old questions I have always had about proof. How do I know if a proof is complete? How do I know if a proof is good?
Many years ago my friend Tyler taught a class about theorem proving using the book Software Foundations. I wrote about this before briefly, but that class raised some other questions: if you’re not able to convince a computer of the proof, does it count as proof? What if you’re able to convince a computer but you don’t understand it yourself?
I still don’t really have the answers, but I decided the following for this attempt:
- I should understand that something I’m supposed to prove is true. I should understand why before attempting a proof.
- I should try to write a proof that would convince me, sometime in the future, when I have forgotten about this.
- I should not worry too much about convincing a real mathematician.
This comes down to the problem that I didn’t have to do any real proofs in college, so I never wrote proofs or had them scrutinized. Writing real proofs is probably at least half or more about having experience reading real proofs, and that isn’t something I spent much time on in college either. This is a bit like trying to write programs without reading programs.
I would say about half of my skill at programming comes from be able to read code and reading other people’s code and stealing their ideas. So to get better at writing proofs, I need to spend time reading proofs, struggling with writing proofs, and then stealing other people’s ideas when I finish them. This is all going to take time.
I would have hoped that formal proof, i.e. software proof using things like Coq and Lean would help with writing informal proofs, the kind that mathematicians like. In practice though, it doesn’t seem to be the case, because A) you might know something is true and not really be able to convince a theorem prover, because you don’t understand enough about the system or how to write the tactics or whatever, and B) it often does seem to be possible to convince the machine that something is true without really knowing what steps it took, thanks to automated tactics.
I spent some time this last week playing The Natural Number Game which is a pretty cool introduction to the Lean theorem prover. I still came away with the feeling that the game of building the proof didn’t necessarily come with a lot of understanding of what I was trying to prove. And I absolutely do not see how to take a book like Introduction to Topology and do my homework with Lean. I just have no clue how you would get started. So that remains an open question: would it be useful to learn Coq or Lean enough to be able to use it to assist with one’s homework in some other advanced class? Or is that just a bridge too far?
Lattices
I learned a little casual abstract algebra from Haskell, but one area I had never heard anything about was lattices, until I read this excellent article from Christopher Alexander called A City is Not a Tree.
Lattices are interesting for a number of reasons, but one that might surprise you is that you often do not have a total ordering between some apparently orderable items. We often want a total ordering, so that we can sort a set, but often we only have a partial ordering—some of the elements come before some of the other elements, but not every pair of elements can be compared.
Lattices turn out to be everywhere once you know about them. I was having a conversation last week about my preferences for a version control system. I’ve used (briefly) CVS, subversion, mercurial, git, Tom Lord’s arch, fossil, and darcs. I have trouble comparing some of these to each other but I have definite preferences between some of them. Because I have a favorite and a least favorite (not using version control at all), my preferences form a lattice. What makes lattices interesting is the notions of infimum (meet) and supremum (join), the idea that no matter which pair of elements you present to me, I can give you another element from the same set which is either below or above the pair you presented. When the items are directly comparable, it’s one of those two items, but if they aren’t, I can still find something else from the set to give you.
Considering my version control preferences, the join of nothing and CVS is CVS, because I would prefer you use something (anything) over nothing. The join of Tom Lord’s arch and CVS is probably git though, because I really didn’t enjoy arch when I used it and CVS has lots of well-known issues.
The book I’m reading, Introduction to Lattice Theory with Computer Science Applications uses lattice theory to solve distributed computing problems. I’m sure there are lots of other interesting applications for it. But even having a name for something causes you to search for it and notice when you have it, creating opportunities to leverage your knowledge.
Another area of abstract algebra I wish I knew more about is group theory, which apparently comes up a lot in particle physics.
Final thoughts
I think probably I will try to take a class this fall with an emphasis on proof. My feeling is that getting better at proof will make it much easier for me to explore these areas of math on my own. And being forced to do it with time constraints will probably make it flow more easily. I guess we’ll see.