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

Hi Hassan,
Just to clarify, my responses below.
michael

On Fri, 5 Dec 2008 15:08:40 -0800
"Hassan Ait-Kaci" <hak@ilog.com> wrote:

> > > 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).


Right. But somebody had to define this extension (both semantics and syntax)
and push it through the WG.


> The other (more problematic) issue is the fact that
> frames may not be nested.

This is a good illustration of the dynamics of the WG process. The original
proposal had nesting, but it was struck down at one of the f2f because people
were concerned that it might be hard to implement and/or understand.
Now consider what it would take to push the general monoid stuff through...


> > > > > 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.

As you said, it is a matter of taste.  What you are proposing is not a simple
local change.  Personally, I do not find the above simpler than what I consider
to be a standard textbook definition (I consulted 3 popular textbooks). I
should also mention that the very first version of the semantic structures in
BLD was formulated by Peter Patel-Schneider.  So, it not just one weirdo like
me who prefers this style.



	cheers
	  --michael

Received on Friday, 5 December 2008 23:32:17 UTC