RE: That other flavour...
I'm glad I prompted Nate to resurface for a moment. Here are my very
cursory notes on his document MIAstandard.pdf of Feb 4, 2013:
Very nice exposition. Bounded and semibounded supported, but Empty is
not an interval, anc comparisons with Empty are unordered. Very nice
explanation of Modal vs Kaucher vs (what we would call) Common, unified
by the Set(interval) operator: { x: min(l,r) <= x <= max(l,r) for [l,r] }
Then proper([l,r]) means Ex(x in Set([l,r])) (l <= r)
improp([l,r]) means Ax(x in Set([l,r])) (l >= r)
There is also the notion of inner and outer digital roundings, and
the lattices meet/join and min/max (the latter has top and bot that
are not members of the set of modal intervals, as l and r cannot be
infinities of the same sign.
Standard MIA only has bounded non-empty intervels; Extended MIA also
has unbounded (but still non-empty) intervals.
Notion of "component splitting" of a box into proper and improper
coordinates. Semantic function extensions of a real function whose
restriction to a box (i.e. Set(box)) is continuous, and subscripted
min/max over proper resp. improper coordinates) are:
f* = [min_p max_i f, max_p min_i f ]
f** = [max_i min_p f, min_i max_p f ]
These are the same if all components are proper, in which case this is
the classical function extension. They are also equal if all components
are improper, but then the result is the improper [max, min].
We always have Dual(f*(X)) \equiv f**(Dual(X))
and: f*(X) \subseteq f**(X)
The semantic functions are inclusion-monotonic.
Join-Meet-Commutable functions have f*(X) = f**(X) -- this includes all
continuous one-dimensional functions, and continuous partially monotonic
two-dimensional functions such as arithmetic operators.
Semantic Theorems on inner Y** and outer Y* estimations of Y.
Syntactic (epxression tree) evaluation uses outer rounding for *-extensions
and inner rounding for **-extensions. Duality allows an inner rounding
computation to be replaced by outher roundings.
Concept of *-interpretability and **-interpretability of a function;
optimality when both hold. Notion of "empty operator" which returns
the non-interval Empty, and is used when "optimality" does not hold,
i.e. one or the other interpretability rule fails.
Tracking decorations EIN, DAC, DEF, GAP and NDF, and static decorations
with lower-case names that are mutually exclusive.
Decorated "elements" include decorated intervals and decorated Empty.
Inclusion order: EIN < DAC < DEF < GAP > NDF > EIN
Quality order: ndf < gap < def < dac < ein
Forgetful operators:
decorated element -> bare interval, bare empty, bare dec
Promotions:
bare X -> (X,dac)
bare Empty -> (Empty, ein)
bare dec -> (Empty, dec)
I encourage everybody to take a serious look.
This was of course NOT written in a manner that would fit as Chapter 3
in the current P1788 draft, but it might have sufficient information to
derive a differential description, with a reference to Nate's document.
Michel.
---Sent: 2013-09-23 18:06:45 UTC