See also: IRC log
<AxelPolleres> yes, I am here
<AxelPolleres> but I have very bad sound quality :-(
<ChrisW> action 303 complete
<AxelPolleres> THat was on me?!
<AxelPolleres> and it is done!
<ChrisW> action 295 continued
<ChrisW> ACTION: christian to ask adrian to update may 22 minutes [recorded in http://www.w3.org/2007/06/12-rif-minutes.html#action01]
<rifbot> Created ACTION-316 - Ask adrian to update may 22 minutes [on Christian de Sainte Marie - due 2007-06-19].
<AxelPolleres> please note: action 296 is done, which was more or less the same as 295.
<ChrisW> RESOLVED: accept minutes of may 29
csma: any updates?
<PaulVincent> PRR - no update
csma: front page of wiki now has first draft of PRR
csma: proposed date is either
last week of August or third week of September (17-21)
... we're looking for offers to host F2F7 during one of these weeks
... deadline is next Tuesday so we can start organizing before vacations
chrisW: looks like we'll be able
to make a proposal
... I prefer end of August but that may not work for Michael
csma: other proposals welcome
csma: point I wanted to make is
that we spent the 2 days unresolving something we had already
... wanted to have enough for second working draft, but didn't get there
... I propose that we should be talking about barest possible core, leaving out extra things like built-ins for now
... we should move into strawman and document mode when discussing something instead of editors doing all the work
... i.e. we propose the text, and editors just have to edit it
<Zakim> sandro, you wanted to mention the idea of core 1.0 and core 2.0
<GaryHallmark> I think csma said to leave out all but the bare mininum set of builtins, not to leave them out entirely
sandro: it's possible for us to define core in phase 1 and then a larger core in phase 2
<GaryHallmark> I suspect we will have to revise the core when we find out that it isn't extensible enough for some dialects
michael: to update the current
document according to the decisions made is pretty simple
(except for travel)
... can't really build a logic by pieces of text and massaging them into document
... I'm against composing a document by discussing pieces of text during telecons
... I'm afraid docment will become mishmash of text
<Hassan> +1 with Michael's analysis
csma: instead of proposing list of builtins, we propose text to go into spec and where it should go
<GaryHallmark> I think the gist is that change proposals should be specific and complete, rather than just "I don't like that", and I say +1
<AxelPolleres> ok, seems we have agreement here! right?
csma: want to avoid spending time discussing a small item where real work is whole document
<Harold> If we want to succeed by F2F7, we must focus on *completing* what we have already achieved through many earlier telecons, actions, and f2f meeings.
csma: regarding F2F6, no minutes yet (don't even have access to resolutions now)
<AxelPolleres> seems doesn't work, have to type.
<AxelPolleres> yes done.
<AxelPolleres> buyt obsolete by the droping of sorts, maybe!
<Harold> TERM ::= Const | Var | Uniterm | List, where List ::= 'list''(' TERM* ')'
<AxelPolleres> how is that different from the function symbol list?
<GaryHallmark> harold, what about head | tail syntax?
<AxelPolleres> done, but also may be obsoluted by decisions at f2f? we should discuss it...
<Harold> Axel, in XML syntax there would be no difference; cf. And' '(' CONDITION* ')'.
<DavidHirtle> (Chris, are you still doing the actions?)
<AxelPolleres> harold: I asked myself whether/how 'list' is different from a local constant 'list'
<Harold> Gary, head | tail syntax could be allowed, too, by introducing the vertical bar "|" in argument sequences as you indicate.
<Harold> Axel, the XML syntax for, e.g., Prolog's list [a,b,c] it would be <List><Const>a</Const><Const>ba</Const><Const>c</Const></List>.
michael: we need to take all
sorts out and put into separate architecture document...
... should be able to do it by end of the month (vacation, etc)
(that was discussion of action 299)
<AxelPolleres> got it, harold, thanks.
<GaryHallmark> harold, by "|" I meant don't we need builtins to select the head and tail of a list object, where head is a non-list term and tail is a list?
<ChrisW> MichaelKifer, can you mute?
<Harold> If we use a <rest> element for the vertical bar "|" in argument sequences, <List> <Var>head</Var> <rest><Var>tail</Var></rest> </List> unifies with <List><Const>a</Const><Const>b</Const><Const>c</Const></List> by binding <Var>head</Var> to <Const>a</Const> and <Var>tail</Var> to <List> <Const>b</Const><Const>c</Const> </List>.
<GaryHallmark> +1 to Harold
<GaryHallmark> Harold, are nested Lists allowed, e.g. <List><List/></List>
csma: as mentioned during f2f, I
have a problem with the current abstract syntax
... sent a proposal yesterday and Gary replied that it was more complicated than necessary
<sandro> Christian's Proposal Syntax Change
csma: document I'm talking about,
please go there
... so we have forall which is subclass of rule and associated to clause
<Harold> Gary, Yes nested Lists would be allowed.
<AxelPolleres> I am at the current draft on wiki
<AxelPolleres> universal quantification in rule bodies is problematic. as is existential in heads. THese two cases are ruled out now What is your concrete suggestion? I am not sure.
csma: awkward to extend it to
case of extensionally quantified variables
... instead of having forall being a subclass of rule etc., I propose that rule has 3 subclasses: forall, implies, atomic
<AxelPolleres> See, what I wrote above. How is universal in bodies than singled out? I don't get it. :-(
<PaulVincent> Qu: why is ForAll a subclass of rule? I'd have thought it a component...
<AllenGinsberg> It should be called something like "Quantifiers" not "ForAll"
<PaulVincent> ... or maybe its the subtype of rule we are talking about?
<Harold> Christian, we decided long ago to have a Forall around every Implies (not following Prolog's quantification convention for top-level rules).
harold: if we have exists in assertions, it is a different semantic language
<AxelPolleres> exists in assertions is NOT Horn.
Harold: But we decided long ago to wrap every Implies (with variables) with Forall.
csma: I agree we
want all variables in an Implies to be explicitely qualitifed.
My syntax changes does not enforce that.
... But the current draft doesn't enforce that at the syntax level, either!
<AllenGinsberg> What if a rule has no variables? Does that mean it has an empty "forall"?
csma: In either case it has to be in the text.
harold: because it's a context-free language, right/
csma: I'm talking about extensibility
harold: right, but you're heading
... later, we can easily add exists to draft
Harold: we can always extend Forall by turning it into Quantifier, where Forall and Exists are kinds of Quantifiers.
csma: I agree, could be done this way... but simpler and clearer to remove redundant clause
Gary: I agree with Axel and Harold's points... this change introduces problems like requiring an id
<PaulVincent> Apologies = offline
Gary: scopedBy introduces a loop in serialization
csma: No, it's just the same thing as "formula"
<sandro> (I would call it "subFormula")
Gary: in that case you serialize the condition, whereas here you refer to a rule previously serialized
sandro: syntactically in XML, forall is an outer element, and x=3 is child element?
<sandro> forall x, p(x) -> q(x)
sandro: gary, does that address problem?
<Harold> Christian, RULE is an (all-uppercase) 'invisible' non-terminal, so not shown in XML serializations.
chrisW: is this resolved?
sandro: not quite sure I understand it...
harold: let's keep the current version; changes aren't really necessary
csma: this doesn't impact semantics, right?
Chris: Harold's point is that current syntax at least FORCES you to have a forall, even though (because of context-freeness) it doesn't enforce that every single variable is quantified.
Gary: csma's syntax allows thing we don't want, like Forall in the body and head of rule.
csma: I thought that would be a good thing!
gary: it seems to allow foralls in body and exists in head...
chrisW: I don't think that's
... implies was just moved up
csma: condition doesn't change, so those bits aren't different.
<AxelPolleres> I don't see how it is simpler. sorry.
chrisW: well, 4 classes instead of 5
csma: this seems to need more discussion
<AxelPolleres> If we just leave it, and the resulting language is the same, I'd rather not discuss it lenghtly, just for the sake of saving one abstract class.
michael: as far as I can see from diagram and ASN, seems like existentials in head and universals in body are allowed
<Harold> Christian, what *other* purpose does Forall have, if not above Implies and ATOMIC?
csma: first diagram defines exists and forall (where they may exist), and second shows where they're allowed
michael: why do we need 2 diagrams?
csma: okay, I see the point of
confusion; I'm a bit confused between meta-modelling level and
... I'll revise the diagrams
gary: could you create an instance document before and after so we see a concrete example?
csma: to avoid dialects defining
different syntactic constructs for the same purpose, we should
have a library of syntactic constructs
... this is the action on Harold
harold: I agree with michael: we
could move multisorted text from core into arch
... use this as a testbed both syntactically and semantically
chrisW: one of the arch
document's goals is to take high level design ideas out of the
core, making it smaller
... arch document should not be critical path for Harold and Michael, so we'll need some more people
csma: is the arch document now clear?
<AxelPolleres> it is clear, but the path is not toally clear to me.
csma: or rather, unclear to anyone?
<AxelPolleres> since we can have restrictions of the core as well, yes?
(proposal to adjourn)
<ChrisW> no problem
This is scribe.perl Revision: 1.128 of Date: 2007/02/23 21:38:13 Check for newer version at http://dev.w3.org/cvsweb/~checkout~/2002/scribe/ Guessing input format: RRSAgent_Text_Format (score 1.00) Succeeded: s/even though it doesn't enforce variables being quantified/even though (because of context-freeness) it doesn't enforce that every single variable is quantified/ Succeeded: s/an example/a concrete example/ Found ScribeNick: DavidHirtle Found Scribe: David Hirtle Default Present: Harold, Francois, Sandro, csma, ChrisW, IgorMozetic, PaulaP, PaulVincent, Allen_Ginsberg, DavidHirtle, AxelPolleres, Leora_Morgenstern, MichaelKifer, Gary_Hallmark, MarkusK, Hassan, Deborah_Nichols, GiorgosStoilos Present: Harold Francois Sandro csma ChrisW IgorMozetic PaulaP PaulVincent Allen_Ginsberg DavidHirtle AxelPolleres Leora_Morgenstern MichaelKifer Gary_Hallmark MarkusK Hassan Deborah_Nichols GiorgosStoilos Regrets: DaveReynolds MohamedZergaoui MichaelSintek JosDeBruijn JeffPan Agenda: http://lists.w3.org/Archives/Public/public-rif-wg/2007Jun/0029.html Got date from IRC log name: 12 Jun 2007 Guessing minutes URL: http://www.w3.org/2007/06/12-rif-minutes.html People with action items: christian[End of scribe.perl diagnostic output]