equal
deleted
inserted
replaced
945 correctness proof of the POSIX value algorithm. Frisch and Cardelli |
945 correctness proof of the POSIX value algorithm. Frisch and Cardelli |
946 introduced an ordering, written $\greedy$, for values and they show that |
946 introduced an ordering, written $\greedy$, for values and they show that |
947 their greedy matching algorithm always produces a maximal element |
947 their greedy matching algorithm always produces a maximal element |
948 according to this ordering (from all possible solutions). The only |
948 according to this ordering (from all possible solutions). The only |
949 difference between their greedy ordering and the ``ordering'' by Sulzmann |
949 difference between their greedy ordering and the ``ordering'' by Sulzmann |
950 and Lu is that GREEDY always prefers a $Left$-value over a $Right-value$. |
950 and Lu is that GREEDY always prefers a $Left$-value over a $Right$-value. |
951 What is interesting for our purposes is that the properties reflexivity, |
951 What is interesting for our purposes is that the properties reflexivity, |
952 totality and transitivity for this GREEDY ordering can be proved |
952 totality and transitivity for this GREEDY ordering can be proved |
953 relatively easily by induction. |
953 relatively easily by induction. |
954 |
954 |
955 These properties of GREEDY, however, do not transfer to POSIX by |
955 These properties of GREEDY, however, do not transfer to POSIX by |