RE: Flavor-independent meaning of decorations
John Pryce wrote:
> On 31 Dec 2012, at 14:33, Nathan T. Hayes wrote:
> > On last note is that, strictly speaking, I think p_ndf only needs to be
> > defined as:
> > p_ndf The restriction of f to X is empty and
> > not p_ein
> > The reason is because p_dac, p_def, and p_gap all require that the
> > restriction of f to X is nonempty. So by definition p_ndf already
precludes
> > them.
> I agree.
>
> >> Or can one replace ein dac def gap on RHS by their
> >> uppercase versions, since it seems to me p_DAC = (p_dac or p_ein), etc?
> >
> > The only reason I may tend to avoid this is it may create a circular
> > dependency: the uppercase (tracking) decorations are defined in terms of
the
> > lowercase (static) decorations. Shouldn't all the lowercase decorations
be
> > defined first? What do you think?
>
> What if you define them in pairs. Is this correct?
> p_EIN The restriction of f to X is defined | p_ein = p_EIN
> and continuous on empty input |
> p_DAC The restriction of f to X is defined | p_dac = p_DAC - p_EIN
> and continuous |
> p_DEF The restriction of f to X is defined | p_def = p_DEF - p_DAC
> p_NDF The restriction of f to X is empty | p_ndf = p_NDF - p_EIN
> p_GAP Always true | p_gap = p_GAP - p_DEF -
p_NDF
>
> using "-" to mean "and not".
>
> Which does revert rather to Arnold's (& my) style, with your uppercase p's
being our
> lowercase ones.
Yes, it appears this gives the same definitions in my old "Decorations as
State Machine" paper, but in an alternative style. I think you could just as
well define the uppercase (tracking) decorations first:
p_EIN The restriction of f to X is defined and continuous
on empty input
p_DAC The restriction of f to X is defined and continuous
p_DEF The restriction of f to X is defined
p_GAP Always true
p_NDF The restriction of f to X is Empty
and then define the lowercase (static) decorations second:
p_ein p_EIN
p_dac p_DAC and not p_EIN
p_def p_DEF and not p_DAC
p_gap p_GAP and not ( p_DEF or p_NDF )
p_ndf p_NDF and not p_EIN
Whatever the case may be, whatever the editorial style that is chosen, the
most important consequence is the universe of all (f,X) pairs is partitioned
into the five disjoint sets of static (lowercase) decorations which have the
linear order:
ein > dac > def > gap > ndf
and the tracking (uppercase) decorations form the containment order:
EIN \subseteq DAC \subseteq DEF \subseteq GAP \supseteq NDF
\supseteq EIN
For evaluation of a real function f over some input X, one then propagates
decorations through the syntax tree of arithmetic operations that define f
by using the "min" rule. We can also propagate decorations through
intersection operation with the "min" rule; and convex hull may be the
"tightest" decoration by containment order that contains both operands. All
of this gives the following implications:
Tracking
Decoration The true mathematical (static) decoration for (f,X)
is...
EIN ein
DAC ein or dac
DEF ein or dac or def
GAP ein or dac or def or gap or ndf
NDF ein or ndf
Nate