ONT Re: Functional Logic
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
FL. Note 4
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
2.1.4. Measure for Measure
An acquaintance with the functions of the umpire operator can be gained
from Tables 13 & 14, where the 2-dimensional case is worked out in full.
The auxiliary notations:
!a!_i f = !Y!<f_i, f>,
!b!_i f = !Y!<f, f_i>,
define two series of measures:
!a!_i, !b!_i : (B^2 -> B) -> B,
incidentally providing compact names for
the column headings of these two Tables.
Table 13. Qualifiers of Implication Ordering: !a!_i f = !Y!<f_i => f>
o------o------o----------o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o
| | x | 1100 | f |a |a |a |a |a |a |a |a |a |a |a |a |a |a |a |a |
| | y | 1010 | |1 |1 |1 |1 |1 |1 |0 |0 |0 |0 |0 |0 |0 |0 |0 |0 |
| f \ | | |5 |4 |3 |2 |1 |0 |9 |8 |7 |6 |5 |4 |3 |2 |1 |0 |
o------o------o----------o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o
| | | | |
| f_0 | 0000 | () | 1 |
| | | | |
| f_1 | 0001 | (x)(y) | 1 1 |
| | | | |
| f_2 | 0010 | (x) y | 1 1 |
| | | | |
| f_3 | 0011 | (x) | 1 1 1 1 |
| | | | |
| f_4 | 0100 | x (y) | 1 1 |
| | | | |
| f_5 | 0101 | (y) | 1 1 1 1 |
| | | | |
| f_6 | 0110 | (x, y) | 1 1 1 1 |
| | | | |
| f_7 | 0111 | (x y) | 1 1 1 1 1 1 1 1 |
| | | | |
| f_8 | 1000 | x y | 1 1 |
| | | | |
| f_9 | 1001 | ((x, y)) | 1 1 1 1 |
| | | | |
| f_10 | 1010 | y | 1 1 1 1 |
| | | | |
| f_11 | 1011 | (x (y)) | 1 1 1 1 1 1 1 1 |
| | | | |
| f_12 | 1100 | x | 1 1 1 1 |
| | | | |
| f_13 | 1101 | ((x) y) | 1 1 1 1 1 1 1 1 |
| | | | |
| f_14 | 1110 | ((x)(y)) | 1 1 1 1 1 1 1 1 |
| | | | |
| f_15 | 1111 | (()) |1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 |
| | | | |
o------o------o----------o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o
Table 14. Qualifiers of Implication Ordering: !b!_i f = !Y!<f => f_i>
o------o------o----------o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o
| | x | 1100 | f |b |b |b |b |b |b |b |b |b |b |b |b |b |b |b |b |
| | y | 1010 | |0 |0 |0 |0 |0 |0 |0 |0 |0 |0 |1 |1 |1 |1 |1 |1 |
| f \ | | |0 |1 |2 |3 |4 |5 |6 |7 |8 |9 |0 |1 |2 |3 |4 |5 |
o------o------o----------o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o
| | | | |
| f_0 | 0000 | () |1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 |
| | | | |
| f_1 | 0001 | (x)(y) | 1 1 1 1 1 1 1 1 |
| | | | |
| f_2 | 0010 | (x) y | 1 1 1 1 1 1 1 1 |
| | | | |
| f_3 | 0011 | (x) | 1 1 1 1 |
| | | | |
| f_4 | 0100 | x (y) | 1 1 1 1 1 1 1 1 |
| | | | |
| f_5 | 0101 | (y) | 1 1 1 1 |
| | | | |
| f_6 | 0110 | (x, y) | 1 1 1 1 |
| | | | |
| f_7 | 0111 | (x y) | 1 1 |
| | | | |
| f_8 | 1000 | x y | 1 1 1 1 1 1 1 1 |
| | | | |
| f_9 | 1001 | ((x, y)) | 1 1 1 1 |
| | | | |
| f_10 | 1010 | y | 1 1 1 1 |
| | | | |
| f_11 | 1011 | (x (y)) | 1 1 |
| | | | |
| f_12 | 1100 | x | 1 1 1 1 |
| | | | |
| f_13 | 1101 | ((x) y) | 1 1 |
| | | | |
| f_14 | 1110 | ((x)(y)) | 1 1 |
| | | | |
| f_15 | 1111 | (()) | 1 |
| | | | |
o------o------o----------o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o--o
Applied to a given proposition f, the qualifiers !a!_i and !b!_i tell whether
f rests "above f_i" or "below f_i", respectively, in the implication ordering.
By way of example, let us trace the effects of several such measures, namely,
those that occupy the limiting positions of the Tables.
!a!_00 f = 1 iff f_00 => f iff 0 => f, hence !a!_00 f = 1 for all f.
!a!_15 f = 1 iff f_15 => f iff 1 => f, hence !a!_15 f = 1 iff f = 1.
!b!_00 f = 1 iff f => f_00 iff f => 0, hence !b!_00 f = 1 iff f = 0.
!b!_15 f = 1 iff f => f_15 iff f => 1, hence !b!_15 f = 1 for all f.
In short, !a!_0 = !b!_15 is a totally indiscriminate measure,
one that accepts all of the propositions f : B^2 -> B, while
!a!_15 and !b!_0 are measures that appreciate the constant
propositions 1 : B^2 -> B and 0 : B^2 -> B, respectively,
above all others.
Finally, in conformity with the use of the fiber notation to
indicate sets of models, it is natural to use notations like
the following to denote classes of propositions that satisfy
the umpires in question:
[| !a!_i |] = (!a!_i)^(-1)(1)
[| !b!_i |] = (!b!_i)^(-1)(1)
[| !Y!_p |] = (!Y!_p)^(-1)(1)
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o