Well-foundedness and lexical coupling (with A.J.M. van Gasteren)

Well-foundedness and lexical coupling.

In AvG88/ EWD1079 - Well-foundedness and the transitive closure- we use, as our definition, that well-foundedness of relation R means that for any predicate P (on the domain of R)

(0) $\left( {\underline{A}y : {P}{y}}\right) \Leftarrow \left( {\underline{A}y : {P}{y}}\right) \Leftarrow \left( {\underline{A}x : x{P}{y} : {P}{x}}\right) )$ . When reading AvG 88/EWD 1079, ATAC raised the question -just like we ourselves had done- whether this definition is more convenient than alternative ones, e.g. that all decreasing chains are of finite length. So as an experiment we then set out to prove some more theorems that so far we had only proved using the decreasing-chains definition. This note records the result of the experiment.

Theorem0 If the components of a lexical coupling are well-founded, so is the lexical coupling.

Theorem1 If a lexical coupling with non-empty domain is well-founded, so are its components.

Denoting both the lexical coupling and its component relations by $c <$ ,we define the former for all(x,a)and(y,b)by

$\left( 1\right) \;x,a < \left( {y,b}\right) \equiv - x < y \vee \left( {x = y \land a < b}\right) .$

$$ . A v G 8 9 / E W D 1 0 8 0 - 1 $$

Proof of Theorem 0

(2) $\left( {\underline{A}y,b : P.y.b}\right) \Leftrightarrow$

$$ (\underline {{\theta}} y, b: P. y. b \Leftarrow (\underline {{\theta}} x, a: (x, a) < (y, b): P. x. a)), $$

given (0) for the component relations, i.e. for any

(3) $\left( {{\underline{\;A}}{y} : Q,y}\right) \Leftarrow \left( {{\underline{\;A}}{y} : Q.y}\right) \Leftarrow \left( {{\underline{\;A}}_{x} : x < y : Q.x}\right)$ (4) $\left( {{\underline{\mathrm{A}}}\mathrm{b} : \mathrm{R},\mathrm{b}}\right) \Leftarrow \left( {{\underline{\mathrm{A}}}\mathrm{b} : \mathrm{R},\mathrm{b}}\right) \Leftarrow \left( {{\underline{\mathrm{A}}}\mathrm{a} : \mathrm{a} < \mathrm{b} : \mathrm{R},\mathrm{a}}\right)$ .

Starting with the antecedent of (2) we calculate

$$ \begin{array}{l} (\underline {{\theta}} y, b: \mathcal {P} _ {y}, b \Leftarrow (\underline {{\theta}} x, a: (x, a) < (y, b): \mathcal {P} _ {x, a})) \ = {{1 } } \ (\underline {{A}} y, b: P _ {y}. b \Leftarrow (\underline {{B}} x, a: x < y \vee (x = y \wedge a < b): P _ {x}. a)) \ = {\mathrm {r a n g e s p l i t t i n g}; \mathrm {o n e - p o i n t r u l e} } \ \underline {{C A}} y, b: P _ {y}. b \Leftarrow \ \end{array} $$

$$ \begin{array}{l} (\underline {{A}} x, a: x < y: P. x. a) \wedge (\underline {{B}} a: a < b: P. y. a) \ = {\mathrm {n e s t i n g a n d p r e d . c a l c . : p r e p a r i n g d i s t r i b u t i o n} } \ \end{array} $$

$$ \begin{array}{l} (\underline {{\theta}} y: (\underline {{\theta}} b: (P _ {y}. b \Leftarrow (\underline {{\theta}} a: a < b: P _ {y}. a)) \Leftarrow \ , \quad (\underline {{\theta}} x, a: x < y: P. x. a) \ \end{array} $$

[\left{ \begin{array}{l} \text{ distributing out antecedent under }\left( {\underline{\mathrm{A}}\mathrm{b}\cdots }\right) ; \ \text{ then (4) with }R \mathrel{\text{:=}} {P}_{y} \text{ on remaining } \ \text{ quantification over }B \end{array}\right. ]

$\left( {\underline{A}y\because \left( {\underline{A}b\because {P}_{.}y.b}\right) \Leftarrow \left( {\underline{A}x,a : x < y : P,x.a}\right) }\right)$

$$ A v G 8 9 / E W D 1 0 8 0 - 2 $$

$= \left{ {\text{nesting,prepar ing for}\left( 3\right) }\right}$

$$ (\underline {{A}} y: (\underline {{A}} b: P _ {y}. b) \Leftarrow (\underline {{A}} x: x < y: (\underline {{A}} a: P _ {x}. a)) $$

$\Rightarrow$ $\left{ \begin{array}{l} \text{(3)} \end{array}\right.$ with $Q.Z \mathrel{\text{:=}} \left( {\underline{\underline{\mathbf{A}}}b : : P.z.b}\right)$ ,for $z = x,y,$ and unnesting

$$ (\underline {{A}} y, b: P _ {y} b) $$

End Proof of Theorem 0

Proof of Theorem1 We have to derive (3) and

(4) from the validity of (2) for all $P$ . Note that the theorem does not hold for lexical couplings with empty domain. Therefore, we ex-pect the property

(5) lexical coupling has non-empty domain $\equiv$ component relations have non-empty domains to come in handy.

Proof of (3) Starting at the antecedent, we get

$$ \begin{array}{l} (\underline {{A}} y: \underline {{Q}}. y) \Leftarrow (\underline {{A}} x: x < y: Q. x)) \ = {\mathrm {n o n - e m p t y r a n g e s}: (5) } \ (\underline {{A}} y, b: \quad Q. y \Leftarrow (\underline {{A}} x, a: x < y: Q. x)) \ = {\mathrm {d e f .} P: Q. y \equiv P. y. c, \mathrm {f o r a l l} y \mathrm {a n d} c (*) } \ (\underline {{A}} y, b: \quad P. y. b \Leftarrow (\underline {{A}} x, a: x < y: P. x. a)) \ \end{array} $$

$\Rightarrow$ {anti-monotonicity, twice, using (1) :

$$ x < y \Rightarrow (x, a) < (y, b) $$

$$ a n t e c e d e n t o f (2) $$

$\Rightarrow$

$$ A v G 8 9 / E W D 1 0 8 0 - 3 $$

$$ \begin{array}{l} \Rightarrow \quad \left{ \begin{array}{l} (2) \end{array} \right} \ (\underline {{A}} y, b: P _ {y} b) \ = \left{\underline {{A}} b: P. y. b \right} = Q. y, f r o m (*) a n d (5) \rbrace \ (A y: A, y) \ \end{array} $$

End Proof of (3)

$$ \begin{array}{l} \mathrm {P r o o f o f (4)} \ (\underline {{\underline {{a}}}} b: \quad R. b \Leftarrow (\underline {{\underline {{a}}}} a: a < b: R. a)) \ = \begin{array}{l} {\left{b y (5), P _ {z} (\underline {{a}} y: P) a n d P _ {z} (\underline {{a}} x: x = y: P), \right.} \ {\mathrm {f o r} y a n d x r e s p e c t i v e l y n o t i n} P \end{array} \ (\underline {{A}} y, b: R. b \Leftarrow (\underline {{A}} x: x = y: (\underline {{A}} a: a < b: R. a)) \ \begin{array}{l}{= {\mathrm {p r e d . c a l c .}; \mathrm {a n d} \quad R. c = P. z. c, \mathrm {f o r a l l} z, c (x) }}\{\left(\exists y, b: P. y. b \rightleftharpoons (\exists x, a: x = y \land a < b: P. x. a)\right)}\end{array} \ \Rightarrow \left{b y (1), (x = y \land a < b) \Rightarrow (x, a) < (y, b) \right} \mathrm {a n t e c e d e n t o f (2)} \ \Rightarrow \quad {(2) } \ (A y, b: P y, b) \ = {(A y: P. y. b) \equiv R. b, b y () a n d (5) } \ \end{array} $$

$$ (\underline {{A}} \underline {{b}}: R. b) $$

End Proof of (4)

End Proof of Theorem 1.

We are grateful to the Eindhoven Tuesday Afternoon Club for useful comments on an earlier version of this note; especially J.C.S.P. van der Woude's insistence that we obey our own rules and provide a heuristically convincing argument is appreciated.

Eindhoven, 18 September 1990

prof.dr. Edsger N. Dyksha Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 U.S.A.

dr. A.J.M. van Gasteron Department of Mathematics and Computing Science University of Groningen P.O.Box 800 9700 AV Groningen The Netherlands