3 ms·

Of course, the alternative hypothesis is that they weren't lying and they did forget it. As someone who majored in math quite successfully within the last decad

Of course, the alternative hypothesis is that they weren't lying and they did forget it. As someone who majored in math quite successfully within the last decade, I can honestly tell you I didn't remember what ":" meant and therefore had trouble parsing the expression. I don't think I forgot intentionally or was lying.

gizmo686 10y ago
As someone currently majoring in mathamatics, I can honestly say this is the first time I have seen ":" used in this way. The "standard" way I would expect to see that would be for the first ":" to be replaced with a "|", and the second one to be replaced with a "," (or omitted entirely). The third ":" does not look out of place, although I would probably omit it, or right it as "st". EDIT: for clarity, I would right the set as: "{f : [1..N ⟶ 1..N] | ∀ y ∈ 1..N , ∃ x ∈ 1..N st f[x]=y}" The ":" in this case indicates that f has the indicated type. As long as I am commenting on my sense of "standard" notation, I should also note that the "[1..N ⟶ 1..N]" notation also seems weird (as in, I have never seen it before). I would expect it to be written as [1..N] ⟶ [1..N]. Perhaps replacing [1..N] with Z_n for the appropriate audience; however the speaker seems to be aware that this is a strange notation, as he commented about it in the beginning. In this particular case, I would probably also omit the entire predicate in favor of writing "onto" above "⟶", which I can do because the particular property being described is common enough to have a name; however this would defeat the point of showing the notion. Once I have entirely omitted the predicate like this, I would probably omit naming f entirely, giving the notation {[1..N] ⟶ [1..N]} (again, with "onto" written above the arrow). Actually, depending on audience, in this particular case I would replace the entire set with either "The symmetric group of order n", "The symmetric group S_n", or just "S_n". The f[x] notation looks a bit weird out of context, but does come up when the distinction between a function and a function application is important (often times f(x) is used as a convention to remind the reader that f is a function)
- pron 10y ago
  Lamport wrote it the way he did because that's the TLA+ notation, and the talk was about TLA+. That formula is actually parsed by the TLA+ tools. Unlike paper math, TLA+ needs to have a precise grammar. I'm really not sure why `|` isn't used in set comprehensions, but I'm guessing that he wanted to keep `:` as "such that" everywhere. `f[x]` is used b/c round parentheses are reserved for operator arguments, and functions aren't operators (the whole thing is based on axiomatic set theory, and in formal math "function" must be something very specific).

gizmo686 10y ago

As someone currently majoring in mathamatics, I can honestly say this is the first time I have seen ":" used in this way. The "standard" way I would expect to see that would be for the first ":" to be replaced with a "|", and the second one to be replaced with a "," (or omitted entirely). The third ":" does not look out of place, although I would probably omit it, or right it as "st". EDIT: for clarity, I would right the set as: "{f : [1..N ⟶ 1..N] | ∀ y ∈ 1..N , ∃ x ∈ 1..N st f[x]=y}" The ":" in this case indicates that f has the indicated type. As long as I am commenting on my sense of "standard" notation, I should also note that the "[1..N ⟶ 1..N]" notation also seems weird (as in, I have never seen it before). I would expect it to be written as [1..N] ⟶ [1..N]. Perhaps replacing [1..N] with Z_n for the appropriate audience; however the speaker seems to be aware that this is a strange notation, as he commented about it in the beginning. In this particular case, I would probably also omit the entire predicate in favor of writing "onto" above "⟶", which I can do because the particular property being described is common enough to have a name; however this would defeat the point of showing the notion. Once I have entirely omitted the predicate like this, I would probably omit naming f entirely, giving the notation {[1..N] ⟶ [1..N]} (again, with "onto" written above the arrow). Actually, depending on audience, in this particular case I would replace the entire set with either "The symmetric group of order n", "The symmetric group S_n", or just "S_n". The f[x] notation looks a bit weird out of context, but does come up when the distinction between a function and a function application is important (often times f(x) is used as a convention to remind the reader that f is a function)

pron 10y ago
Lamport wrote it the way he did because that's the TLA+ notation, and the talk was about TLA+. That formula is actually parsed by the TLA+ tools. Unlike paper math, TLA+ needs to have a precise grammar. I'm really not sure why `|` isn't used in set comprehensions, but I'm guessing that he wanted to keep `:` as "such that" everywhere. `f[x]` is used b/c round parentheses are reserved for operator arguments, and functions aren't operators (the whole thing is based on axiomatic set theory, and in formal math "function" must be something very specific).