IRC log of rif on 2008-11-24
Timestamps are in UTC.
- 16:02:21 [RRSAgent]
- RRSAgent has joined #rif
- 16:02:21 [RRSAgent]
- logging to http://www.w3.org/2008/11/24-rif-irc
- 16:02:39 [DaveReynolds]
- zakim, this is rif
- 16:02:39 [Zakim]
- ok, DaveReynolds; that matches SW_RIF(CORE)11:00AM
- 16:03:13 [LeoraMorgenstern]
- LeoraMorgenstern has joined #rif
- 16:03:43 [Zakim]
- +LeoraMorgenstern
- 16:05:27 [Michael_Kifer]
- Michael_Kifer has joined #rif
- 16:05:44 [Zakim]
- +Gary
- 16:05:54 [Zakim]
- +kifer
- 16:06:16 [Gary_Hallmark]
- Gary_Hallmark has joined #rif
- 16:07:15 [DaveReynolds]
- ScribeNick: DaveReynolds
- 16:07:32 [Harold]
- http://www.w3.org/2005/rules/wiki/index.php?title=Core&action=history
- 16:08:43 [Harold]
- Michael: Shortened conformance section.
- 16:08:52 [Harold]
- ... Things that were not defined before.
- 16:09:08 [Harold]
- ... Issues
- 16:09:18 [Harold]
- Dave; One by one.
- 16:09:30 [Harold]
- Section 2.1:
- 16:10:18 [Harold]
- ISSUE: Did we really decide that ## cannot occur at all or that it can occur only in the rule bodies?
- 16:10:18 [trackbot]
- Created ISSUE-84 - Did we really decide that ## cannot occur at all or that it can occur only in the rule bodies? ; please complete additional details at http://www.w3.org/2005/rules/wg/track/issues/84/edit .
- 16:11:16 [Harold]
- Section 2.3 :
- 16:11:28 [Harold]
- ISSUE: What was decided about external functions?
- 16:11:29 [trackbot]
- Created ISSUE-85 - What was decided about external functions? ; please complete additional details at http://www.w3.org/2005/rules/wg/track/issues/85/edit .
- 16:11:52 [DaveReynolds]
- ROPOSED: Core should keep unrestricted equality and
- 16:11:54 [DaveReynolds]
- external function and predicate calls in rule bodies and keep external
- 16:11:56 [DaveReynolds]
- functions calls in rule heads.
- 16:12:27 [Harold]
- s/ROPOSED: /PROPOSED: /
- 16:13:06 [Harold]
- Michael: Will add to syntax.
- 16:13:31 [Harold]
- But there is an issue with matching vs. unification.
- 16:13:44 [Harold]
- Christian gave an example.
- 16:13:56 [Michael_Kifer]
- From:
- 16:14:03 [Michael_Kifer]
- ex:A(2)
- 16:14:09 [DaveReynolds]
- ScribeNick: Harold
- 16:14:11 [Michael_Kifer]
- ex:A(?x) :- ex:A(?x - 1)
- 16:14:17 [Michael_Kifer]
- Infer: ex:A(3).
- 16:15:43 [Harold]
- ex:A(?x) :- ex:A(External(?x - 1))
- 16:16:01 [Michael_Kifer]
- No way a PRD implementation can pass that test case, as far as I can see, because, PRD does not allow binding ?x to 3, in that case.
- 16:16:40 [Harold]
- Because it goes strictly bottom-up.
- 16:16:56 [DaveReynolds]
- ex:A(?x) :- ex:A(?y), subtract(?y, 1, ?x)
- 16:17:08 [Harold]
- So ?x has no value in the premise.
- 16:18:02 [Harold]
- Gary: Translator could do some rewriting.
- 16:18:34 [Harold]
- Michael: Can we do better than putting things into implementation notes?
- 16:19:35 [Harold]
- ... Dave's rewriting would work.
- 16:19:50 [Harold]
- ... But may not be obvious to readers when it can be done like that.
- 16:20:16 [Harold]
- Dave: Using equality?
- 16:20:51 [Harold]
- Michael: Maybe add an example about how to implement this stuff.
- 16:21:07 [Harold]
- ... (Better than an implementation notes.)
- 16:21:22 [Harold]
- Gary: Are there non-tractable cases?
- 16:21:43 [Harold]
- Michael: Blow-up correlates with # of built-ins per rule.
- 16:22:05 [Harold]
- Gary: Still have to make sure that built-ins have kinds of inverses.
- 16:22:46 [Harold]
- Michael: Always replace it with an equation; then see if further predicates can be introduced.
- 16:22:50 [Michael_Kifer]
- ex:A(?x) :- ex:A(?y), ?y=?x-1
- 16:23:23 [Harold]
- Dave: Could restrict syntax.
- 16:23:39 [DaveReynolds]
- TERM = Constant | Variable and Equal ::= TERM '=' (TERM | 'External' '(' Atom ')' )
- 16:24:09 [Harold]
- ... simplify to implement these restrictions.
- 16:24:26 [Harold]
- Michael/Dave: No strong preference.
- 16:24:47 [Harold]
- Alternatives:
- 16:25:10 [Harold]
- 1) Unrestricted use of external functions.
- 16:25:22 [Harold]
- 2) Prohibit external functions.
- 16:25:45 [Harold]
- 3) Only allow external functions in equalities in the premises.
- 16:26:18 [Harold]
- Gary: Tricky part to solve those equations.
- 16:26:29 [Harold]
- Michael: Not allowed in PRD.
- 16:26:53 [Harold]
- Gary: It's ok there, but: Translator need to do some work.
- 16:27:15 [Harold]
- ... have to start of with a 'pattern'.
- 16:27:40 [Harold]
- ... then have to refer to variables bound in the pattern.
- 16:27:56 [Harold]
- ... Above first solve ?x, then ?y.
- 16:28:47 [Harold]
- ... If just cater for min translation, then Core becomes too small to be interesting.
- 16:29:14 [Harold]
- Michael: Well, alternative 3) could be interesting.
- 16:29:30 [Harold]
- ... puts burdon on translator.
- 16:29:49 [Harold]
- ... In PRD you can express this anyway.
- 16:30:38 [Harold]
- ... In Prolog you cannot embed functions anyway but use 'is' primitive.
- 16:30:53 [Harold]
- ... Most logic languages work like that.
- 16:32:42 [Harold]
- Dave: We could update the EBNF a bit.
- 16:32:46 [Harold]
- Gary: Yes.
- 16:32:54 [Harold]
- Michael: Yes.
- 16:33:27 [Harold]
- Gary: One for fwd, one for bwd chaining.
- 16:34:12 [Harold]
- Michael: If there is no (inverse) function like "-", then the problem doesn't come up.
- 16:34:23 [Harold]
- ... Hence not a big deal.
- 16:34:53 [Harold]
- Gary: The translator gets x on one side, y on the other side, then rephrases that.
- 16:35:17 [Harold]
- ... In preparation for production rules.
- 16:35:32 [Harold]
- ... Can always do that. That's fine.
- 16:35:46 [Harold]
- ... Rest is pretty trivial compared to that.
- 16:36:12 [Harold]
- ... Service we're doing is setting things up in a convertible way.
- 16:36:48 [Harold]
- Michael: OK, problem doesn't go away.
- 16:37:29 [Harold]
- ... Same things happens even if we just use predicates.
- 16:37:44 [Harold]
- ... Then it would be binding patterns (modes).
- 16:38:18 [Harold]
- ... Real qu is if all built-ins can be inverted.
- 16:38:38 [Harold]
- ... A kind of requirement on DTB.
- 16:38:46 [Harold]
- ... Or, other solution can be found.
- 16:39:00 [Harold]
- ... Maybe explain it in upcoming PRD telecon.
- 16:39:36 [Harold]
- ... Fine with all 'solutions', except they are not complete solutions.
- 16:40:00 [Harold]
- .Dave: Since we have no binding patterns, it's a syntactic problem.
- 16:40:24 [Harold]
- ... not in BLD, not in PRD, ...
- 16:41:16 [Harold]
- Michael: In some cases there may be nothing better than raising errors.
- 16:41:39 [Harold]
- .... Totally diff engines cannot totally interoperate.
- 16:41:53 [Harold]
- ... EVery lang. need to do some synt. analysis.
- 16:42:45 [Harold]
- Dave: Explain reordering for each target language?\
- 16:43:19 [Harold]
- Michael: We can keep it as is and in worst case give errors if no synt. analysis.
- 16:44:17 [Harold]
- Gary: Just as easily as we can do y = x-1 we could also do 1 = x-y.
- 16:44:58 [Harold]
- Typically only one variable should be free, all others bound.
- 16:45:20 [Harold]
- Gary: How powerful an equ solver do we need/want.
- 16:46:14 [Harold]
- We need to keep in mind all things we want to add to Core will also need to make it to BLD (LC) and PRD.
- 16:47:30 [Harold]
- Dave; Semantics of BLD is fine. In practice you could not have a complete implementation. Same for PRD. It's 'only' a matter of implementations.
- 16:47:47 [Harold]
- s/Dave;/Dave:/
- 16:48:14 [Harold]
- ... Different classes of dialects..
- 16:48:32 [Harold]
- Let's look at both versions of text/EBNF.
- 16:48:38 [DaveReynolds]
- At the moment we have:
- 16:48:39 [Harold]
- Then compare and decide.
- 16:48:40 [DaveReynolds]
- TERM ::= IRIMETA? (Const | Var | 'External' '(' Atom ')' )
- 16:48:46 [DaveReynolds]
- Equal ::= TERM '=' TERM
- 16:49:35 [DaveReynolds]
- So option three would be:
- 16:49:44 [DaveReynolds]
- >TERM ::= IRIMETA? (Const | Var)
- 16:49:55 [DaveReynolds]
- Equal ::= TERM '=' (TERM | 'External' '(' Atom ')' )
- 16:51:38 [Harold]
- If we could have External on EITHER side, then would be still symmetric.
- 16:52:26 [Harold]
- Equal ::= Equal ::= TERM '=' (TERM | 'External' '(' Atom ')' ) | (TERM | 'External' '(' Atom ')' ) '=' TERM
- 16:52:51 [Harold]
- s/Equal ::= Equal/Equal /
- 16:53:53 [Harold]
- Dave: Will change EBNF to reflect this, Michael change the text correspondingly.
- 16:54:02 [Harold]
- ... Eds note
- 16:54:24 [Harold]
- Michael: Will put it in.
- 16:55:40 [Harold]
- Section 4
- 16:55:57 [Harold]
- Re: ISSUE: sub might not be allowed. This depends on the resolution of the issue
- 16:56:18 [Harold]
- regarding the subclass relationship.
- 16:56:37 [Harold]
- Dave: Should be easy.
- 16:57:31 [Harold]
- Section 5.1:
- 16:58:11 [Harold]
- "A subformula of a condition formula is called disjunctive subformula if it appears within a Disjunction. "
- 16:58:35 [Harold]
- Leora: Looks clearer now.
- 16:58:44 [Harold]
- Dave: Fixed two places.
- 16:59:02 [Harold]
- Michael: Shortened issue I wrote.
- 16:59:36 [Harold]
- ... What does "non-disjunctive atomic subformula" really mean?
- 16:59:44 [Harold]
- Dave: Was defined earlier.
- 17:00:10 [Harold]
- ... Using "surrounding disjunction", so withIN.
- 17:00:28 [Harold]
- ... Relevant for Safeness condition.
- 17:00:49 [Harold]
- Michael: Does not really say it.
- 17:01:11 [Harold]
- Leora: Nomenclature is kind of odd. Use more descriptive term.
- 17:01:46 [Harold]
- .... Then attach the "disj" there. Would not require so much preparatory definitions.
- 17:02:16 [Harold]
- .... Should be readable sequentially without need for remembering too many techn terms.
- 17:02:48 [Harold]
- Michael: Sounds almost as if someone changed their mind in the middle of the psi/phi sentence.
- 17:03:05 [Harold]
- ... Original one had psi only at the end of sentence.
- 17:03:57 [Harold]
- Dave: Maybe drop phi. Will check. Better phrasing.
- 17:04:17 [Harold]
- .... This evening.
- 17:05:00 [Harold]
- Michael: Also my work this evening.
- 17:05:15 [Harold]
- When to consolidate both edits?
- 17:06:14 [Harold]
- Michael: Would be fine with Dave's edits.
- 17:06:56 [Harold]
- Everyone should say what should still be done before freeze.
- 17:08:22 [Harold]
- Michael: Current section on PRD is very early, so we need eds note its REALLY preliminary.
- 17:09:40 [DaveReynolds]
- rrsagent, make minutes public
- 17:09:40 [RRSAgent]
- I'm logging. I don't understand 'make minutes public', DaveReynolds. Try /msg RRSAgent help
- 17:09:43 [Zakim]
- -Gary
- 17:10:09 [Zakim]
- -kifer
- 17:10:10 [Zakim]
- -LeoraMorgenstern
- 17:10:40 [DaveReynolds]
- rrsagent, draft minutes
- 17:10:40 [RRSAgent]
- I have made the request to generate http://www.w3.org/2008/11/24-rif-minutes.html DaveReynolds
- 17:10:52 [DaveReynolds]
- rrsagenta, make minutes public
- 17:10:57 [DaveReynolds]
- rrsagent, make minutes public
- 17:10:57 [RRSAgent]
- I'm logging. I don't understand 'make minutes public', DaveReynolds. Try /msg RRSAgent help
- 17:11:07 [DaveReynolds]
- rrsagent, make log public
- 17:11:25 [DaveReynolds]
- rrsagent, draft minutes
- 17:11:25 [RRSAgent]
- I have made the request to generate http://www.w3.org/2008/11/24-rif-minutes.html DaveReynolds
- 17:11:46 [DaveReynolds]
- zakim, who was present?
- 17:11:46 [Zakim]
- I don't understand your question, DaveReynolds.
- 17:13:01 [DaveReynolds]
- zakim, who is here?
- 17:13:14 [Zakim]
- On the phone I see DaveReynolds, Harold
- 17:13:15 [Zakim]
- On IRC I see Michael_Kifer, LeoraMorgenstern, RRSAgent, DaveReynolds, Harold, sandro, trackbot, Zakim
- 17:13:16 [DaveReynolds]
- zakim, list attendees
- 17:13:16 [Zakim]
- As of this point the attendees have been Harold, LeoraMorgenstern, Gary, kifer, DaveReynolds
- 17:13:23 [DaveReynolds]
- rrsagent, draft minutes
- 17:13:23 [RRSAgent]
- I have made the request to generate http://www.w3.org/2008/11/24-rif-minutes.html DaveReynolds
- 17:14:02 [DaveReynolds]
- Chair: Harold
- 17:14:04 [DaveReynolds]
- rrsagent, draft minutes
- 17:14:04 [RRSAgent]
- I have made the request to generate http://www.w3.org/2008/11/24-rif-minutes.html DaveReynolds
- 17:14:21 [Zakim]
- -DaveReynolds
- 17:14:25 [Zakim]
- -Harold
- 17:14:27 [Zakim]
- SW_RIF(CORE)11:00AM has ended
- 17:14:28 [Zakim]
- Attendees were Harold, LeoraMorgenstern, Gary, kifer, DaveReynolds