union and munion pattern about documentation HOT 24 CLOSED

Perhaps there should be a "whenever possible" in there somewhere, but surely it would be understood that matching against a set with a single value must result in one set being empty?

from documentation.

Well, the following is VDMJ's result, and VDMTools also produce the same result.
I'm supportive for it, too.

p let {} union {a,b} in set {{1,2}} in mk_(a, b)
= mk_(1, 2)
Executed in 0.075 secs.

I think a reasonable constraint is "Neither union, munion nor ^ matches against empty set/map/sequence.", which implies "Either subclass/submap/subsequence is non-empty".

from documentation.

But aren't we confusing two things here? The example you give above matches using an empty set pattern, but the first example is talking about binding an empty set to a non-empty pattern. I think the documentation is just trying to say that when binding a set value using a union pattern, the left and right parts will be distinct and ("whenever possible") non-empty. If you use an empty set pattern with a union, then it seems natural that, in effect, the "{} union" disappears, just leaving the RHS to match the set.

from documentation.

Interesting. I didn't think about reducing {} union. My understanding was, matching a union pattern against a set value will generate all possible partitions into two subsets and then try matching left-hand side subpattern against one subset and the right-hand side against another subset one by one.

I thought an empty set pattern "{}" and an empty set value pattern "({})" behave the same.
There seems difference between VDMJ and VDMTools about it.
In VDMJ,

> p cases {1,2}: {} union {a,b} -> 1, otherwise -> 2 end
= 1
Executed in 0.002 secs.
> p cases {1,2}: ({}) union {a,b} -> 1, otherwise -> 2 end
= 2
Executed in 0.005 secs.

In VDMTools,

>> p cases {1,2}: {} union {a,b} -> 1, otherwise -> 2 end
1
>> p cases {1,2}: ({}) union {a,b} -> 1, otherwise -> 2 end
1

from documentation.

You're right about the matching process - and the various alternatives are tried when the union is wrapped in larger patterns that may match only some partitions of the set.

I can't see how {1,2} can possibly match ({}) union {a,b}, since the value does not include an empty set element. The LHS has a literal empty-set element in it, surely? So this union can only match values with three elements. Or am I missing something? :)

from documentation.

I just tried this in VDMJ. You need ({{}}) in the LHS to match element {} in the value, since the LHS has to be an expression that is a set which contains the value to match. But in that case, you can happily do the following:

> p let ({{}}) union a = {{},1} in a
= {1}
Executed in 0.027 secs. 

from documentation.

I just tried this in VDMJ. You need ({{}}) in the LHS to match element {} in the value, since the LHS has to be an expression that is a set which contains the value to match.

I think ({}) union {a,b} should match against {1,2} when the interpreter partitions {1,2} into {} and {1,2} and ({}) matches against {} and {a,b} against {1,2}. My suggestion is to change the explanation of union pattern in the LRM from

In the VDM interpreters the two subsets will always be chosen such that they are non-empty and disjoint.

to

A union pattern does not match to the empty set. In the VDM interpreters the two disjoint subsets will be chosen

.Maybe this should further be discussed in the LB?
I think we are not modifying the language spec, but just making clarification. :-)

from documentation.

What's the status on this? Still awaiting LB discussion?

If so, we should add an action for the next meeting now that the board is back

from documentation.

Luis, thanks for reminding me this issue. I think we better discuss here and then propose an action to the LB.

from documentation.

Great, thanks.

On 31 January 2016 at 23:01, Tomohiro Oda [email protected] wrote:

Luis, thanks for reminding me this issue. Yes, I'll post to the ML.

—
Reply to this email directly or view it on GitHub
#9 (comment)
.

from documentation.

Louis, sorry for confusion. I first posted to tell I'll post this issue to the ML, but I changed my mind and edited my post to keep discussion here. I think we should make a tentative solution here before making it an LB action.
So, I'd like to hear more from you and nick in particular. What do you think about the natural language explanation of set/map union patterns?

from documentation.

Well, the text you suggested is not precisely true. There is at least one union pattern that matches with the empty set.

 p let {} union {} = {} in {}
= {}
Executed in 0.005 secs. 

We can argue about whether or not it's really a match. But the interpreter does not report pattern match failed.

I agree that the text as written is slightly ambiguous and the bit about the subsets being non-empty is clearly wrong. I also think the first part: The two patterns are matched to a partition of two subsets of a set. is a bit vague.

BTW, why is the language manual talking about VDM interpreters? That's a tool issue. Or does the language itself prescribe that the subsets must be disjoint?

How about...

A set union pattern fits only set values. The two patterns will match disjoint subsets of the value.

@nickbattle thoughts?

from documentation.

Yes, there are tool issues in the LRM to make them compatible while the language itself is specified rather loosely. Maybe we better "unify" those semantics into more tool oriented way. Please note that there are tools other than interpreters.

For example, the ISO specifies set union patterns very loose so that a pair of subsets may overlap and may be empty. We need extra constraints to make tools feasible. (I don't know if this classic definition is still effective in VDM10.)

tr_iso.vdmsl.pdf p.141

.2-.3  If the value is a set value, it is 'chopped' into all possible pairs of sets which union is equal to
    the set value (notice that it is not required that these set-values are non-empty or disjoint) .

and the definition of ChopSetVal in p.142

145.1 ChopSetVal(MkTag('set', elem_s)) ~
.2 { (MkTag( 'set', el_s1), MkTag( 'set', el_s2)) I el_s1, el_s2 E SET_ VAL·
.3 el_s1 U el_s2 = elem_s}

from documentation.

There is at least one union pattern that matches with the empty set.

You are right. And we still need "In the interpreter" phrase as described in my previous comment.

How about

A set union pattern fits only set values. In the VDM interpreters, the two patterns will match disjoint subsets of the value.

from documentation.

I got an interesting result.
In VDMJ,

> p let {} union {} union {} = {} in 1
= 1
Executed in 0.001 secs. 
> p let ({} union {}) union {} = {} in 1
Error 4125: Set union pattern does not match expression in 'DEFAULT' (console) at line 1:19

In VDMTools,

>> p let [] ^ [] = [] in 1
1
>> p let ({} union {}) union {} = {} in 1
1

Empty is so interesting as zen masters say :-)

from documentation.

Interesting... :-) I'll look at that match failure, though presumably it's because the LHS is an "expression pattern" when you add the brackets, I think. Not sure why that's different though!

from documentation.

Yes. The expression pattern on the LHS was being considered as "length 1" (which is the default length for pattern matches). But actually, as this example shows, the length of an expression is really "ANY" (a special value meaning that we don't know the length). Adding this to the ExpressionPattern class produces the result expected:

> p let ({} union {}) union {} = {} in 1
= 1
Executed in 0.185 secs. 

from documentation.

The same problem/fix appies to Overture. So I think this is probably a valid bug and we should commit the fix.

from documentation.

Created an issue in the overture repo for this: overturetool/overture#502

from documentation.

Nick,
This fix should reproduce VDMTools' behavior described in #9 (comment)

from documentation.

Yes, the fix makes all the tools the same: VDMTools, VDMJ and Overture.

from documentation.

And ViennaTalk :-)
I found this issue when implementing a Smalltalk code generator.

from documentation.

Now that the corresponding bug is fixed we can close this issue, right? :)

from documentation.

Ah, sorry, I'll close this.

from documentation.