A word on BIDMAS

Maybe it’s not called that in other countries, but in the UK BIDMAS (which I swear was “BODMAS” when I was at school, or maybe I just went to a weird school) was the rule that was used to figure out how to work out what things like 1+2*3-4/(5+6-7*8-9) meant. The BIDMAS rule was that B for Brackets came first, and then there’s this I which might stand for “indices” i.e. ^, and then division, multiplication, addition and subtraction. There seemed to be some disagreement amongst my own children (all of whom have learnt this at school over the last few years) as to whether the “DM” in BIDMAS meant that division had to be done before multiplication, or whether division and multiplication had equal “strength”. I ultimately realised that I was not entirely sure I understood this BIDMAS thing myself! I am pretty sure that BIDMAS doesn’t mean that addition must be done before subtraction, otherwise a-b+c would come out to be a-(b+c), whereas I am almost certain that it is supposed to mean (a-b)+c. [Interestingly though, it seemed to me that doing all divisions before all multiplications, from left to right, seems to give the same answer as treating division and multiplication with the same weight.]

We see from this discussion that these pieces of notation like + and *, and of course other symbols such as , and had better also have some sort of BIDMAS rule. Furthermore, we had also better know whether we evaluate them from left to right or from right to left, because sometimes this matters and sometimes it depends on the operator! For example 10-5-4 is (10-5)-4=1 and not 10-(5-4)=9, however if you type 2^1^2 into your favourite computer algebra package (or 2**1**2 if you’re using python) then the chances are you’re going to get 2^(1^2)=2^1=2 rather than (2^1)^2=2^2=4. Indeed, you can check that Lean thinks it’s 2:


#eval 2 ^ 1 ^ 2 -- Lean says 2
#reduce 2 ^ 1 ^ 2 -- still 2

How does this actually work then?

For any piece of notation like -, we need to know two things: First, its power (in the sense that BIDMAS says that * has more power than -; the power of an operator is a natural number) and secondly we need to know its associativity (we need to know whether a-b-c means (a-b)-c or a-(b-c)). It turns out that this is all you need to know. Lean’s parser is a so-called Pratt parser but all you really need to know is how Lean figures out the power (technically called the “left binding power”) and associativity of all the operators you run into. These operators include functions like nat.add, and notation like + (note in particular that even though nat.add 2 3 means the same as 2 + 3, the parser treats them differently). Note also that even though (a+b)+c=a+(b+c), Lean still has to know exactly which one is meant by a+b+c; the fact that they are equal is a theorem rather than being true by definition.

The first rule you need to know is that functions have very high power — they eat the next thing they see and that’s it.


#eval nat.add 3 nat.add 4 5 -- error

Functions are greedy. They eat the next thing presented to them and only afterwards check that it has the right flavour. The first nat.add eats 3, and then it eats the second nat.add and chokes because nat.add isn’t a natural number. You have to fix it with brackets, which have the highest power of all:


#eval nat.add 3 (nat.add 4 5) -- evaluates to 12

So that’s brackets and functions. Now what about notation? When notation is defined, its power is also defined. You can see the power of some notation by looking at at the numbers printed out with Lean’s #print notation command. For example


#print notation +
-- _ `+`:65 _:65 := has_add.add #1 #0

It’s the 65’s we need to understand here. The first number 65 tells you that `+` has power 65. The second number 65 tells you that + is left associative, that is, a+b+c=(a+b)+c by definition. Why? Well, in practice that second number is either equal to the first one (meaning the notation is left associative) or one less (meaning right associative). For example


#print notation ^
-- _ `^`:80 _:79 := has_pow.pow #1 #0

The power notation has a higher power than addition, as expected, but 79 is one less than 80, meaning that it’s right associative, as we saw above. Functions and brackets have power over 1000, by the way.

To learn more about left binding power and how Pratt parsers really work, e.g. to learn what the second number actually means and why it’s either equal to or one less than the first number, try the links on the Wikipedia website. But for Lean users who just want to figure out how things are being parsed, this trick should pretty much always tell you what you need to know. It’s worth just typing


#print notation

and looking at all the output — you’ll learn that ^ has power 80, * and / have power 70, and + and - have power 65, which tells you that Lean knows BIDMAS (and that addition and subtraction do indeed have the same power). Interestingly, we also learn that = has power 50. Had it ever occurred to you that = also needed a binding power? Lean also needs to know what P = Q = R means! It turns out that = is left associative, so 1 = 2 = (1 = 2) is true, by reflexivity.

If anyone has run into Lean’s (or Haskell’s) $ as an alternative for brackets, the way it works is that f $ x is just defined to be f x, but $ has power 1, which is so low that everything else gets evaluated first. For example


#eval nat.add 3 $ nat.add 4 5

works! Lean evaluates the $ at the very end, after it’s figured out that nat.add 4 5 is 9, so this time the addition succeeds.

The one gotcha I have run into is that the comma in ∀ (x : X), P x also has a super-low power (it has power 0 in fact), meaning that the innocent-looking


example (P Q : ℕ → Prop) :
∀ x, P x ∧ Q x → ∀ x, Q x ∧ P x := sorry

doesn’t mean what I would instinctively think it meant: Lean brackets it as ∀ x, (P x ∧ Q x → ∀ x, Q x ∧ P x), because has power 25, bigger than the power of the comma. To get this:


example (P Q : ℕ → Prop) :
(∀ x, P x ∧ Q x) → ∀ x, Q x ∧ P x := sorry

you have to add those brackets in explictly.

Advertisements

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College (and beyond) trained in the art of formalising mathematics on a computer.
This entry was posted in Learning Lean, Uncategorized. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s