In trying to prove some interesting properties about theories relating to multimethods, I stumbled upon this fact that completely invalidates them. I'm embarassed to post it here, since it is so simple and obvious that I should have seen it sooner. But, alas, I was cursed by my hubris, not verifying that the most essential properties held, and just assuming that they did. This is why mathematicians insist on being rigorous!
So, let's illustrate by example. Let's say we have a theory Ring{^T} that requires that ^T have a ring structure. We have a role Int for integers, and a role Nat for naturals. Let's also call the set of integers Z and the set of naturals N. Clearly N is a subset of Z.
Given Ring{Int} (the integers form a ring),
Int{Z} and Nat{N} by definition
Ring{^T} <= Int{^T} # expand model definition
N subset Z implies Int{N}, so Int{N} # role relation
Ring{N} since Int{N}.
OK, I'm at a loss here. Naturals don't form a ring because they lack the number zero? Is that right? If so, that seems straightforward enough. However, I don't know what you mean when you wrote that even though Naturals are rings, you seem to have proven they are. I certainly don't know what that means in relation to the code you posted.
Taking a guess, it seems what you're saying is that for a given set S which satisfies condition C, no arbitrary subset of S is necessarily guaranteed to satisfy C but you've accidentally implied that in your theory. Thus, any time you declare a subset of something, your theory implemenation must ensure that constraints the set obeys are also met by the subset?
As for how roles fit into this, would the theory implementation also need to ensure that the roles can operate within said constraints? Hell, am I even making sense? I only have a tenuous grasp of what you're referring to and I suspect that a large stumbling block is my not understanding your syntax for theories. If you care to explain, please be gentle. It's been many years since I've honed my math skills
Re:I don't grok the syntax
luqui on 2005-11-19T08:24:28
> Naturals don't form a ring because they lack the
> number zero?
This is somewhat beside the point, but that is one reason, yes. The other reason is that there are elements (namely, all of them:-) that don't have additive inverses.
> Taking a guess, it seems what you're saying is
> that for a given set S which satisfies condition
> C, no arbitrary subset of S is necessarily
> guaranteed to satisfy C but you've accidentally
> implied that in your theory.
Precisely. It turns out that that's how I (tried to) define roles. The thing that makes a theory a role is that any subset of a set that satisfies a role also satisfies that role.
I'll explain the syntax a bit, even though in my new formulation it will mean something different.
^T represents any set: it is an unconstrained variable. Foo{^T} is a *predicate* on that set. And <= is a poor name for "given" or something (it's supposed to look like a backward "implies"). Basically, the expression ^T <= Foo{^T} can represent any set whose Foo constraint is satisfied.
The place where the error came in:
Ring{^T} < Num{^T}
Means "the Ring constraint is satisfied on a set ^T when the Num constraint is", or, interpreting the language a bit, "a set is a ring if all of its elements are numbers", which is clearly wrong.
As far as the new formulation, I am somewhat satisfied (though disappointed, as I no longer have a masters thesis) that it reduces to a minimal generalization of F<: polymorphic typing. That is, there is already a well-established body of literature on the subject, which means that Perl 6 is more likely to get it right.