Teaching dependent type theory to 4 year olds via mathematics

We had a family Zoom chat today and I ended up talking to my relative Casper, who is 4 and likes maths. He asked me to give him some maths questions. I thought 5+5 was a good place to start, and we could go on from there depending on responses. He confidently informed me that 5+5 was 10, and that 5-5 was zero. For 5*5 he asked me “is that five fives?” and I said yes, and he asked me “Is that 5 lots of 5?” and I said yes, and then he began to count. “1,2,3,4,5. 6,7,8,9,10. 11,12,13,14,15. 16,17,18,19,20. 21,22,23,24,25. It’s 25!” he said. I guess he’s proved this by refl. Every natural number is succ (succ (succ (...(succ zero))...) so to evaluate one of them, you just break it down into this canonical normal form. He did not know what division was, so I thought it was time to move on from 5.

I figured that if he didn’t know his 5 times table we needed to be careful with multiplication, in case of overflow errors, so I decided I would go lower. I next asked him 0+0, 0-0 and 0*0 (“so that’s zero lots of zero?” Yes. “So that’s zero zeros?” Yes). He got them all right, and similarly for 1+1, 1-1 and 1*1. I then thought we could try 0 and 1 together, so I asked him 0+1 to which he confidently replied 1, and 0-1, to which he equally confidently replied 0.

This answer really made me sit up. Because Lean thinks it’s zero too.

#eval 0 - 1 
/-
0
-/

I am pretty sure that a couple of years ago I would have told him that he was wrong, possibly with a glint in my eye, and then tried to interest him in integers. Now I am no longer sure that he is wrong. I am more convinced that what has happened here is that Casper has internalised some form of Peano’s axioms for arithmetic. He knows ℕ. In some sense this is what I have been testing. He knows that every natural is succ succ … succ 0, and then for some reason he has to learn a song that goes with it, with a rigid rhythmical beat and written in 10/4 time: “One, two, three four, five, six, seven, eight, nine, ten. Eleven, twelve,…” and so on ad infinitum, some kind of system which is important for computation but is currently not of interest to me. Also, Casper knows that there’s something called subtraction, and when given junk input such as 0-1 he has attempted to make some sense of it as best he could, just like what the functional programmers who like all functions to be total have done.

We then went onto something else. I asked him what 29+58 was and he essentially said that it was too big to calculate. I asked him if he thought that whatever it was, it was the same as 58+29, and he confidently said it was, even though he did not have a clue what the answer was. I asked him how he was so sure but I did not get a coherent answer.

I asked him what three twos were, and he counted “1, 2, 3, 4, 5, 6“. Three lots of two is 6. I then asked him what two threes were and he immediately replied 6 and I asked him if he’d done the calculation and he said no, two threes were the same as three twos. I asked him why but all he could say was that it was obvious. It’s simp. I asked him if he was thinking about a rectangle and he said no. So he knows simp and refl.

I then did quite a mean thing on him, I did overflow his multiplication buffer. I asked him what ten 3’s were. We spent ages getting there, and he needed help, because he hasn’t learnt how to sing the song in 3/4 time yet. But eventually refl proved that 10*3=30. I then asked him if he thought 3*10=10*3 and he was confident that it was. I then asked him what 3 tens were and whilst he didn’t immediately do this, he knew a song (in 4/4) which started at “one ten is10 (rest)” and finished at “ten tens-are-a hun dred.”. Using the song, we figured out pretty quickly what three tens were, and deduced that ten 3’s were 30 again. I then asked him what ten sevens were, and we talked about how how difficult it would be to sing the song in 7/4 and how long the song would be, and then we talked together through the argument that it was also “obviously” seven tens, so by the song it was seventy; apparently the fact that seventy sounds similar to 7 (even though thirty doesn’t sound that much like 3) is evidence that the patterns in the counting song can be helpful to humans who want to calculate.

I then remembered the junk subtraction answer, so I thought I’d try him on another function which returns junk in Lean, namely pred, the “number before” function on the naturals. I asked him what the number before 3 was, and he said 2. He was also confident that the number before 2 was 1, and the number before 1 was 0. I then asked him what the number before 0 was and he thought a bit and then said….”1?”.

pred is defined by recursion in Lean. We have pred (succ a) = a, and pred 0 is defined to be 0, because if you follow Lean’s “make all functions total, it’s easier for programmers” convention then it has to be something. But the choice of the actual value of pred 0 is probably not seriously used in Lean, and they could have defined pred 0 to be 1 or 37 and probably not much would break, and what did break would probably be easily fixed. Because of whining linter I recently needed to supply a junk value to Lean (it wanted me to prove that the quotient of a ring by an ideal was not the empty set) and I supplied 37 as the witness. pred is a fundamental function defined by recursion, as far as computer scientists are concerned. So why is it not even mentioned in the natural number game? Because you can’t really define functions by induction, you define them by recursion, and I don’t want to start getting involved in new recursive definitions, because this sort of thing cannot go within a begin end block. I could have decided to explain pred but I would have had to address the issue of pred 0 not being error and I realised that actually there was always a “mathematical workaround”. By this I mean the following. The natural proof of succ_inj uses pred, for example. The successor function is injective. The proof using pred is easy. But I tell people in the natural number game that succ_inj is an axiom, as is zero_ne_succ, and now we mathematicians seem to be able to develop a huge amount of theory without ever even defining subtraction. We don’t really want to use Lean’s natural number subtraction. We know that 0 ≠ junk is true by definition but unfortunately `0-0=0-1` in Lean, which is not right.

We then talked about the number line a bit, and I then told him about a level in the 2d Mario franchise where the exit is way off to the right but right at the beginning you can completely counterintuitively go off to the left and pick up some bonus stuff. I then told him that there were some other kinds of numbers which he hadn’t learnt about yet, and I said they were called the integers (note: not “the negative numbers”). I said that the integers included all the numbers he knew already, and some new ones. I told him that in the integers, the number before 0 was -1. I then asked him what he thought the number before -1 would be and he said “-2?” And I told him he was right and asked him what the number before -2 was and he confidently said -3, and we did this for a bit and chatted about negative numbers in general, and then I asked him what the number before -9 was and he said -10. I then asked him what the number before -99 was and he said -100 and then I asked him what the number before -999 was and he said he didn’t know that one and did I want to play Monopoly. I took this as a sign that it was time to stop, and we agreed to play a game of monopoly via this online video chat, and then it turned out that he didn’t know any of the rules of monopoly (he’d just found the box on the floor) and he couldn’t read either, so he just put the figures on random places on the board and we talked about the figures, and what we could see on the board, and what was in the monopoly box, and the maths lesson was over.

I was pretty appalled when I saw Lean’ s definition of int, a.k.a. ℤ. It is so ugly. There are two constructors, one of_nat n which takes a natural number and returns the integer (an invisible function, set up to be a coercion), and the one called something really weird like neg_one_of_nat n which takes in a natural and returns the integer , complete with hideous notation. This definition somehow arrogantly assumes some special symmetry of the integers about the point . The mathematician’s definition, that it’s a quotient of by the equivalence relation , a.k.a. the localisation of the additive monoid of naturals at itself (i.e. adding additive inverses to every element). This definition is a thing of beauty. The symmetry is never broken. It is the canonical definition. But even though this definition as a quotient is the most beautiful definition, classifying as it does the integers up to unique isomorphism because of the universal property of localisation (thanks so much Amelia Livingston), implementation decisions are system specific and int in Lean is the concrete inductive type with two constructors and there’s nothing we can do about this. So mathematically I am kind of embarassed to say that today I basically taught Lean’s definition of int to a kid, just as an experiment.

Another weird thing is that Lean has a really ugly proof of a+b=b+a in int but for some reason this is going to be “obvious” when negative numbers are taught to him in school, and will not need a proof. I guess ac_refl will do it.

When Casper had to go, I told him before he left to ask his parents what the number before -9 was. I think it’s a pretty tricky question if you’re caught off-guard. I told him that negative numbers were like mirror world. Is there educational research about how children model numbers? What different ideas do they have about ℕ before they even start to learn their multiplication tables? Should we teach them induction now, before they are crushed by having to learn so many long and boring songs telling them things like six sevens are 42, because of the belief in the education system currently that memorising this is somehow important in the year 2020 when most teenage kids have a calculator app in their pocket.

Casper loves my daughter Kezia’s art. He says “everything is alive except the rainbow”.

Advertisement