Re: semantics of OPTIONAL/LeftJoin

Dear Andy

I  wonder if you could also clarify the official formal semantics of OPTIONAL. If I understand the intention correctly, then LeftJoin(Ω1, Ω2, expr) should contain a representation of **each** solution mapping μ1 from Ω1 (either extended with some information from Ω2 or not). More precisely, 

 - if there is μ2 in Ω2 such that μ2 is compatible with μ1 and their merge satisfies expr then each such merge is included in LeftJoin(Ω1, Ω2, expr);

 - otherwise, if there is no μ2 in Ω2 such that μ2 is compatible with μ1 and their merge satisfies expr, then μ1 is included in LeftJoin(Ω1, Ω2, expr).

If this understanding is correct then there is a slight problem with the definition of Diff: the condition in Diff(Ω1, Ω2, expr) does not appear to be the complement of the condition in Filter(expr, Join(Ω1, Ω2)). More precisely, if we denote the merge of μ1 and μ2 by μ, then `expr(μ) is an expression that has an effective boolean value of false' is not the complement of `expr(μ) has an effective boolean value of true': according to Section 17.2.2, if an argument of a subexpression is unbound then the EBV is a type error. To illustrate, consider 

Ω1 = { (?X -> :a) }, Ω2 = { (?X -> :a), (?X -> :b, ?Y -> 30) } and F = ?Y = 30.

Then Join(Ω1,Ω2) = { (?X -> :a) } and so Filter(F, Join(Ω1,Ω2)) is empty because the EBV is a type error (not true). Also, Diff(Ω1, Ω2, F) is empty because μ1 = (?X -> :a) in Ω1 has a solution mapping in Ω2 that is compatible with it (the merge coincides with μ1) but F(?X -> :a) has an EBV of a type error because ?Y is not bound. Therefore, the solution mapping μ1 from Ω1 is not represented in any way in LeftJoin(Ω1, Ω2, F). 

Such behaviour does not seem to correspond to the intention (as described above) and it also differs from LEFT JOIN in SQL. I was wondering whether this is a mistake or my understanding of the intention in incorrect. If it is a mistake then it could be corrected by replacing `expr(merge(μ, μ')) has an effective boolean value of false' in the definition of Diff by the following 

'expr(merge(μ, μ')) does not have an effective boolean value of true'

Probably, it is also worth explaining that `does not have an EBV of true' means that the EBV is either false or a type error. It might also make sense to slightly rephrase the whole definition of Diff:

Diff(Ω1, Ω2, expr) = { μ | μ in Ω1 and expr(merge(μ, μ')) does not have an effective boolean value of true for all μ′ in Ω2 such that μ and μ′ are compatible  }

Best regards
Roman

Received on Thursday, 25 June 2015 11:52:19 UTC