RE: [PRD] Action 659 (on hak) completed

>  Hi Hassan,
>  here are my responses to your comments to my comments to your comments.

Hi Michael,

Here are my responses to your responses to my comments to your comments
to my comments. I hope this is my last round on these points ... ;-)

> Maybe this was the source of the confusion?

No. I was wrong. I had simply misread. The definition is no longer confusing.

> There was only one vote, years ago, when it was decided to introduce this
> restriction. At that time full implications of this decision were not obvious
> (at least to me). In the past year I tried to raise this issue at least twice
> in F2Fs, but nobody was interested.

Not at the F2Fs I was at (few and far between that I could attend I know).

> > Be that as it may, this semantics conflicts with the freedom of using
> > frames for representing objects in the presence of multiple occurrences
> > of a given field.
> > The most general approach is to define it using a
> > collection semantics over a commutative monoid. That monoid could very
> > well be idempotent to yield the equivalence you have built in (and which
> > could be the overridable default). However, it is less restrictive to
> > parametrize the semantics up to a consumer-specifiable function collecting
> > multiple values of a same field.
> 
> It is a set semantics. You cannot just parametrize the semantics.
> You need to make this monoid explicit in the syntax, which would be an
> extension of what we have.

This is precisely what I said: you built in a set semantics (i.e., an
idempotent commutative monoid), but why not also allow a bag semantics
(i.e., an non-idempotent commutative monoid), or any other interpreted
collection composition (i.e., sum, etc...)? Yes, I understand that this
would be an extension of what you have defined - but it is a slight one,
a compatible one (since more general), and a useful one (for those
systems that do not use F-logic).

At any rate, this debate is just part of the more concerning adequacy of
frames to model objects (in the usual sense - wherein a set semantics is
not built-in and where collection classes such as lists, sets, bags are
commonly available). The other (more problematic) issue is the fact that
frames may not be nested.

> > > > 2.1.2.2 Interpretation of condition formulas
> > > >
> > > >   - Quoting: "Existence: TVal_I(Exists ?v1 ... ?vn (\phi)) = t if and
> > > >     only if for some I*, described below, TVal_I*(?) = t.  Here I* is a
> > > >     semantic structure of the form <TV, DTS, D, D_ind, D_pred, I_C,
> > > >     I*_V, I_P, I_frame, I_NP, I_sub, I_isa, I_=, I_external, I_truth>,
> > > >     which is exactly like I, except that the mapping I*_V, is used
> > > >     instead of I_V.  I*_V is defined to coincide with I_V on all
> > > >     variables except, possibly, on ?v1,...,?vn."
> > > >
> > > >     Why so complicated? Why not simply rephrase that as, "Existence:
> > > >     TVal_I(Exists ?v1 ... ?vn (\phi)) = t iff TVal_I(\sigma(\phi)) = t
> > > >     for some variable valuation \sigma\ : Var -> D_ind.
> > >
> > > This is also possible. But then the notion of \sigma(\phi) has to be defined
> > > somewhere earlier. Does not save any space (although with some refactoring of
> > > the text it might be possible to save some).
> >
> > First of all, that would make the definition much *simpler* and easier to
> > read, and therefore to understand. Second, it does save space: \sigma(\phi)
> > need not be any further defined - it is the formula results after applying
> > the valuation \sigma\ to \phi.
> 
> I doubt it will save any space or is simpler. The definition used is a
> standard one for these quantifiers (e.g., in Enderton or Mendelson).
> 
> Moreover, what you are proposing is also not quite correct: sigma should be a
> function that maps v1,...,vn only. And then we would have to define not only
> what TVal_I(\phi) is but also what TVal_I(\sigma(\phi)) is. Thinking of it
> more, your proposal would have made the definitions much longer.

Allow me to persist: there are many alternative formulations that are
much simpler than, and just as precise and formally correct as, your (or
Enderton's or whoever's) formulation for capturing the formal semantics
of FOL WFF's. (See, e.g., the attached notes' Section 9.3, Subsection 9.3.2,
Definition 9.3.5 - Semantics of WFF's - which uses a Tarskian set-theoretic
mapping interpreting a formula in the Boolean lattices of sets of variable
valuations - i.e., as a set of variable valuations.)

My point is that I contend that most readers are likely to balk at how
contrived your formulation is for expressing something somehow as simple
and intuitive as basic naive set theory. Perhaps it is a matter of taste,
but I find direct algebraic semantics a la Tarski much simpler and easier
to justify.

>         regards
>           --michael

Cheers,

-hak
--
Hassan Aït-Kaci  *  ILOG, Inc. - Product Division R&D
http://koala.ilog.fr/wiki/bin/view/Main/HassanAitKaci