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