NOTE: use Perl; is on undef hiatus. You can read content, but you can't post it. More info will be forthcoming forthcomingly.

## All the Perl that's Practical to Extract and Report

### Journal of luqui (5770)

Friday November 18, 2005
05:55 PM

### theory.pod sucks

[ #27646 ]

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}.

But the naturals do not form a ring (under integer operations), though I seemed to have proven that they do. The error came in when I "expanded the model definition" from Ring{Int} to Ring{^T} <= Int{^T}.

This can be fixed. The changes necessary to fix this are very minor from the point of view of the theory user, but very major from the point of view of the theorist. In particular, they imply that theory expressions can no longer be reduced to first-order constraints on unnamed types. Instead, the system becomes unbounded-order, which is a bummer for the implementor.

However, I have that unbounded-order system almost entirely formulated in my mind. I'm pretty sure I can keep the benefits of theories while maintaining the solvability of an explicitly annotated system (we know that completely inferring a system this complex is equivalent to the halting problem and thus undecidable). I hope that it is also inferrable "most of the time". Updates soon.

The Fine Print: The following comments are owned by whoever posted them. We are not responsible for them in any way.

Full
Abbreviated
Hidden
• #### I don't grok the syntax(Score:2)

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

• #### Re:I don't grok the syntax(Score:1)

> 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 h