[Inquiry] Re: Functional Logic

[Jon Awbrey]

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

FL.  Note 2

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

2.1.2.  Higher Order Propositions and Logical Operators (n = 2)

By way of reviewing notation and preparing to extend it to
higher order universes of discourse, let us first consider
the universe of discourse X% = [!X!] = [x_1, x_2] = [x, y],
based on two logical features or boolean variables x and y.

1.  The points of X% are collected in the space:

    X   =   <|x, y|>   =   {<x, y>}   ~=~   B^2.

    In other words, written out in full:

    X   =   {<"(x)", "(y)">,
             <"(x)", " y ">,
             <" x ", "(y)">,
             <" x ", " y ">}

    X  ~=~  {<0, 0>,
             <0, 1>,
             <1, 0>,
             <1, 1>}

2.  The propositions of X% make up the space:

    X^  =  (X -> B)  =  {f : X -> B}  ~=~  (B^2 -> B).

As always, it is frequently convenient to omit a few of the
finer markings of distinctions among isomorphic structures,
so long as one is aware of their presence and knows when
it is crucial to call upon them again.

The next higher order universe of discourse that is built on X% is
X%^2 = [X%] = [[x, y]], which may be developed in the following way.
The propositions of X% become the points of X%^2, and the mappings
of the type m : (X -> B) -> B become the propositions of X%^2.
In addition, it is convenient to equip the discussion with with
a selected set of higher order operators on propositions, all
of which have the form w : (B^2 -> B)^k -> B.

To save a few words in the remainder of this discussion, I will use the terms
"measure" and "qualifier" to refer to all types of "higher order" propositions
and operators.  To describe the present arrangement in picturesque terms, the
propositions of [x, y] may be regarded as a gallery of sixteen venn diagrams,
while the measures m : (X -> B) -> B are analogous to a body of judges or
a collection of critical viewers, each of whom evaluates each picture as
a whole and reports the ones that find favor or not.  In this way, each
judge m_j partitions the gallery of pictures into two aesthetic portions,
the pictures (m_j)^(-1)(1) that m_j likes and the pictures (m_j)^(-1)(0)
that m_j dislikes.

There are 2^16 = 65536 measures of type m : (B^2 -> B) -> B.
Table 12 introduces the first sixteen of these measures in the
fashion of the higher order truth table that I set out before.
The column headed "m_j" shows the values of the measure m_j on
each of the propositions f_i : B^2 -> B, for i = 0 to 15, with
a blank entry in the Table being optional for a value of zero.
The arrangement of measures that continues in accord with this
plan will be referred to as the "standard ordering" of measures.
In this scheme of things, the index j of the measure m_j is the
decimal equivalent of the bit string that is associated with
m_j's functional values, which can be obtained in turn by
reading the j^th column of binary digits in the Table as
the corresponding range of boolean values, taking them
in order from bottom to top.

Table 12.  Higher Order Propositions (n = 2)
o------o------o----------o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o
|  | x | 1100 |    f     |m|m|m|m|m|m|m|m|m|m|m|m|m|m|m|m|.|
|  | 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-o
|      |      |          |                                 |
| f_0  | 0000 |    ()    |0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1  |
|      |      |          |                                 |
| f_1  | 0001 |  (x)(y)  |    1 1 0 0 1 1 0 0 1 1 0 0 1 1  |
|      |      |          |                                 |
| f_2  | 0010 |  (x) y   |        1 1 1 1 0 0 0 0 1 1 1 1  |
|      |      |          |                                 |
| f_3  | 0011 |  (x)     |                1 1 1 1 1 1 1 1  |
|      |      |          |                                 |
| f_4  | 0100 |   x (y)  |                                 |
|      |      |          |                                 |
| f_5  | 0101 |     (y)  |                                 |
|      |      |          |                                 |
| f_6  | 0110 |  (x, y)  |                                 |
|      |      |          |                                 |
| f_7  | 0111 |  (x  y)  |                                 |
|      |      |          |                                 |
o------o------o----------o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o
|      |      |          |                                 |
| f_8  | 1000 |   x  y   |                                 |
|      |      |          |                                 |
| f_9  | 1001 | ((x, y)) |                                 |
|      |      |          |                                 |
| f_10 | 1010 |      y   |                                 |
|      |      |          |                                 |
| f_11 | 1011 |  (x (y)) |                                 |
|      |      |          |                                 |
| f_12 | 1100 |   x      |                                 |
|      |      |          |                                 |
| f_13 | 1101 | ((x) y)  |                                 |
|      |      |          |                                 |
| f_14 | 1110 | ((x)(y)) |                                 |
|      |      |          |                                 |
| f_15 | 1111 |   (())   |                                 |
|      |      |          |                                 |
o------o------o----------o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o-o

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o