Change loss function semantics for indexes

[wenkokke]

My intuition says...

foreach i.
  1 < i and i < 9 =>
    prop (
      network X ! i
    )

...should translate to something like...

lossBigAnd(
  lossProp(
    network(X)[i]
  )
  for i
  in range(0, n)
  if 1 < i and i < 9
)

...but if I understand the current translation actually translates this to...

lossBigAnd(
  lossImplies(
    lossAnd(
      indicator(1 < i),
      indicator(i < 9)
    ),
    lossProp(
      network(X)[i]
    )
  for i
  in range(0, n)
)

...which has a completely different and arguably unintuitive semantics.

[wenkokke]

To solve this, we should separated logical operations for properties and for "slices"...

-- embedding slices into booleans
SliceToBool :: Slice -> Bool

-- splitting boolean connectives out into boolean and slice variants
And :: Bool -> Bool -> Bool
AndSlice :: Slice -> Slice -> Slice
Implies :: Bool -> Bool -> Bool
ImpliesSlice :: Slice -> Slice -> Slice
Not :: Bool -> Bool
NotSlice :: Slice -> Slice
Or :: Bool -> Bool -> Bool
OrSlice :: Slice -> Slice -> Slice

-- changing the types of comparisons on indexes
EqIndex :: Index -> Index -> Slice
GeIndex :: Index -> Index -> Slice
GtIndex :: Index -> Index -> Slice
LeIndex :: Index -> Index -> Slice
LtIndex :: Index -> Index -> Slice
NeIndex :: Index -> Index -> Slice

For the immediate future, we can interpret Slice as a bool that consists only of comparisons on values of type Index, and interpret Bool as Rat, for the loss function semantics, and instantiate it as Never on the Python side to indicate the fact that these should never be returned as part of a loss function. This lets us separate out their interpretation for TensorFlow, which means we get (1) fast graph-based operations, and (2) sensible semantics for indexes.

In the future, we should interpret Slice as numpy index arrays, i.e., Array[int] where int is restricted to 0 and 1. This interpretation requires a little bit of work to push the logical operations on slices down into the call to indices.

[MatthewDaggitt]

Okay, so after further consideration:

• By default all boolean operations should remain boolean.
• Only when reaching comparisons on rationals, should we switch over to converting booleans as rationals.
• When going back up the tree and we're combining a boolean and a rational then we use the DL to cast the boolean to a rational and proceed upwards. Otherwise it should be interpreted as simply the boolean operation.