Conceptual progress
Today's exercise: (starting) work on an example formula to grind through the constraint/SAT solution. After writing out lots of tedious copy-paste formulae by hand (I thought pencil/paper would let me "play with" the constraint system more directly, and once I'm done writing things out it might, but ugh...), I've come to the following conclusion (writing by hand may not have been a bad idea, tedious writing means lots of time to just stare and ponder):
The type constraints use types with no GLB to express boolean incompatibility - a boolean variable may not be T and F; a type variable may not have an upper bound of both [m : []] and [m : [m : []]]. Selftypes and the context operator are used for conditional - if a variable U is selftype, then U{V} becomes V; otherwise it stays as U. Chains of subtype relations are setup with U{V} (for various Us and Vs) at each intermediate step, terminating in various incompatible upper bounds. The variable constrained at the bottom is given one upper bound or the other depending on which intervening U variables are assigned to selftype in the constraint solution. Hence, selftype corresponds to falsehood and all other types to truth in the correspondence between SAT and the core selftype constraints. (Choice of falsehood vs truth is most likely just convenience.)
This still does not provide the solution to SAT, but does demonstrate the underlying correspondence between the type system and this NP-complete problem: both the type system and SAT formulae have underlying notions of conditionals and mutual exclusion, and not enough power to express much else.
More tomorrow. Nothing checked into SVN tonight, the above conclusions are my work-product.
The type constraints use types with no GLB to express boolean incompatibility - a boolean variable may not be T and F; a type variable may not have an upper bound of both [m : []] and [m : [m : []]]. Selftypes and the context operator are used for conditional - if a variable U is selftype, then U{V} becomes V; otherwise it stays as U. Chains of subtype relations are setup with U{V} (for various Us and Vs) at each intermediate step, terminating in various incompatible upper bounds. The variable constrained at the bottom is given one upper bound or the other depending on which intervening U variables are assigned to selftype in the constraint solution. Hence, selftype corresponds to falsehood and all other types to truth in the correspondence between SAT and the core selftype constraints. (Choice of falsehood vs truth is most likely just convenience.)
This still does not provide the solution to SAT, but does demonstrate the underlying correspondence between the type system and this NP-complete problem: both the type system and SAT formulae have underlying notions of conditionals and mutual exclusion, and not enough power to express much else.
More tomorrow. Nothing checked into SVN tonight, the above conclusions are my work-product.
posted by pnkfelix at 9:08 PM
3 Comments:
Re: U{V}. . .
I'm interpreting U and V as unification variables in the constraint system (though I'm not sure if "unification variable" is the right term if we're doing more general constraint solving than Robinson's unification).
You say that if U is selftype, then U{V} goes to V; otherwise it stays as U. Did you mean that U{V} stays as U{V} ? Or does it really go to U? If I'm interpreting this all the right way, I would think that you would need a proof that U cannot be selftype before you could turn U{V} into U alone.
U and V are used, in different points in the paper, for both type variables and unification variables, which is unnecessarily confusing. But the context notation is using them as metasyntactic variables for types; constraint variables standing for types work just as well. So it is meaningful to instantiate them to real types and/or type variables, such as [m : X]{[m : selftype]}.
So, if U and V are types such that V is never selftype, then U{V} means V if U is selftype, and V otherwise. They do take care never to use this notation in a context where V might be selftype.
Okay, I've read the part where this notation gets introduced now, and I think I understand what its about.
I'm putting this in a marginpar comment in the paper (to ensure it gets addressed), but I thought that the Blog might also be an appropriate place to debate this.
Here is the paragraph of explanation in the paper:
The notation \(B\{A\}\) is used to provide context for selftypes in the typing
rules, so that selftype cannot be used in meaningless position (a position that
has no ``self''). It is defined to mean \(A\) if \(B\) is \(\self\), or \(B\)
otherwise. Context notation is not defined when \(A\) is \(\self\).
Here is my response:
\fmarnote{This explanation may be misleading.
There \emph{is} a self in e.g. (Method Call); what \(B\{A\}\) does (in my mind) is
\emph{substitution} of the {\bf actual} A for the {\bf formal} \(\self\), in the case where
\(B = \self\). Is that the same as ``providing context''? To me, \(\self\) does not
cease to have meaning, but it \emph{does} change what meaning it may have, since
our p.o.v. may have changed. So perhaps that is the same as providing context\ldots
}
Post a Comment
<< Home