Fix text around least upper bound.

docs/language/dartLangSpec.tex

Index: docs/language/dartLangSpec.tex
diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex
index 62dba6983699c047c42906215f334947d686c81b..a08ff5706fcdd92e289135772e69564776587fae 100644
--- a/docs/language/dartLangSpec.tex
+++ b/docs/language/dartLangSpec.tex
@@ -7791,8 +7791,17 @@ Let $T$ be the declared type of a declaration $d$, as it appears in the program
 
 \LMHash{}
 % does this diverge in some cases?
-Given two interfaces $I$ and $J$, let $S_I$ be the set of superinterfaces of $I$,  let $S_J$ be the set of superinterfaces of $J$ and let $S =  (I \cup S_I) \cap (J \cup S_J)$.  Furthermore, we define $S_n = \{T | T \in S  \wedge depth(T) =n\}$ for any finite $n$ %, and $k=max(depth(T_1), \ldots, depth(T_m)), T_i \in S, i \in 1..m$,
-where $depth(T)$ is the number of steps in the longest inheritance path from $T$ to \code{Object}. Let $q$ be the largest number such that $S_q$ has cardinality one. The least upper bound of $I$ and $J$ is the sole element of  $S_q$.
+Given two interfaces $I$ and $J$,
+let $S_I$ be the set of superinterfaces of $I$,
+let $S_J$ be the set of superinterfaces of $J$
+and let $S =  (\{I\} \cup S_I) \cap (\{J\} \cup S_J)$.
+Furthermore,
+we define $S_n = \{T | T \in S \wedge depth(T) = n\}$ for any finite $n$
+where $depth(T)$ is the number of steps in the longest inheritance path

[eernst, 2017/04/05 11:47:30]

How lucky, `inheritance path` is never defined, so we can make it solve the
halting problem. ;-)

I believe it must be the length of the longest path to `Object` in the
superinterface graph (which is a subgraph of what I usually call "the clause
based supertype graph", it just omits all mixins and their superinterfaces).

To avoid the substantial extra verbiage, I think we can leave it as it is, but
it might be a good idea to add a comment saying these things, briefly, such that
we remind ourselves next time we look.

[Lasse Reichstein Nielsen, 2017/04/05 12:08:59]

I noticed the same thing, and decided not to touch it now. Adding a comment for
posterity.

+from $T$ to \code{Object}.
+Let $q$ be the largest number such that $S_q$ has cardinality one,
+which must exists because $S_0$ is $\{\code{Object}\}$.

[eernst, 2017/04/05 11:47:30]

Typo: `exist`.

[Lasse Reichstein Nielsen, 2017/04/05 12:08:59]

Done.

+The least upper bound of $I$ and $J$ is the sole element of $S_q$.
 
 \LMHash{}
 The least upper bound of \DYNAMIC{} and any type $T$ is \DYNAMIC{}.
@@ -7801,7 +7810,8 @@ The least upper bound of $\bot$ and any type $T$ is $T$.
 Let $U$ be a type variable with upper bound $B$. The least upper bound of $U$ and a type $T \ne \bot$ is the least upper bound of $B$ and $T$.
 
 \LMHash{}
-The least upper bound relation is symmetric and reflexive.
+The least upper bound function is commutative and idempotent,
+but it is not associative.

[Lasse Reichstein Nielsen, 2017/04/05 09:38:31]

Only real change is this line and adding { and } around I and J in the union
expressions above. The rest is just reflowing and removing spurious whitespace.

[eernst, 2017/04/05 11:47:30]

I think `commutative` is commonly associated with binary operators, and a page
like http://math.stackexchange.com/questions/185471/commutative-functions
actually indicates that it's called 'symmetric' for functions. As far as I can
see, idempotent is being used for functions as well as operators.

But the text uses the full phrase `least upper bound` every time (only once does
it say that it's a 'relation', and that's being changed anyway), so I believe we
are free to decide that it's an operator, and we can then say 'The least upper
bound operator is commutative and idempotent'.

[Lasse Reichstein Nielsen, 2017/04/05 12:09:00]

Done, except using "operation" instead of "operator" (the latter, to me, feels
like it's defining something that hasn't been defined yet).

 
 % Function types