On 09/27/2010 12:25 AM, Patrick Browne wrote:
Alexander Solla wrote:
On 09/26/2010 01:32 PM, Patrick Browne wrote:
/
Bigger how? Under logical implication and its computational analogue?
That is to say, do you want the model to be more SPECIFIC, describing a
smaller class of objects more richly (i.e, with "more" logical
implications to be made) or do you want the model to be more GENERAL,
and contain the less specific submodels? This is how "forcing" works.
My idea of bigger is based on the import modes and parameterized modules
of the Maude/CafeOBJ languages, where smaller theories are used to
construct larger theories (and/or objects). In these languages I guess
theories (loose specifications or interfaces) correspond to your
*logical implication* and objects (or tight specification) correspond to
*computation* at the ordinary programming level. The axioms of the
theories must hold at the programming level.
Well, my question was more along the lines of "do you want bigger (more
specific) theories (and so more "specific" models to interpret them)?"
or do you want to generalize from a given theory? To do the latter with
Haskell, you might create a module that allows exporting your
"axiom/interface" functions. And maybe create a wrapper that drops
axioms/interfaces/constraints. This is assuming you've organized your
modules to embody specific theories (an assumption not usually true of
my code, at least under this strict interpretation).
To become more specific, you would just import the a module and add new
axiom/interface functions.
Doing similar constructions with type classes is possible. I think you
might have to use witness types (or even a nice functorial wrapper
around your target value in the original algebra, or both) to do
generalizations of type classes. For example:
class Uneditable obj where
a :: a -> obj
b :: b -> obj
class Refactored obj witness where
a' :: Maybe (a -> obj)
b' :: Maybe (a -> obj)
data EmptyFilter -- I think the name of the extension needed for this is
'EmptyDataDecls'
data NoA
data NoB
instance Uneditable obj => Refactored obj EmptyFilter where a' = Just a;
b' = Just b
instance Uneditable obj => Refactored obj NoA where a' = Nothing; b' =
Just b
etc
You would be using the Maybe part to "switch" functions/axioms on and
off. The witness type links the obj type to the intended generalization
of Uneditable.
By the way, this is a decent example of forcing for types: given a type
that satisfies a theory (that is, whose values are models for the
theory), you generate a set of "names" which links the type to "new"
theories that are related in a fairly obvious way (in this case, via
Maybe). This represents an embedding of the new theory in the old
theory. (And, dually, it represents an embedding of the old model in
the new one) There's more to it than that, insofar as there is stuff to
be proved. But Haskell does it for you.
What does the term *forcing* mean?
Forcing is a technique to create models from axiomatizations. It is the
countable (and beyond) extension of creating a model by adding elements
piecewise, assuming they satisfy the theory. Indeed, you end up using
"filters" (the dual to an ideal) to ensure you get rid of all the
elements that don't satisfy a model. The wikipedia page goes over some
of this in term so of constructing a model in terms of a language over a
theory for the model, and reinterpreting the new language in terms of
the old one.
http://en.wikipedia.org/wiki/Forcing_(mathematics)
See:
http://books.google.ie/books?id=Q0H-n4Wz2ssC&pg=PA41&lpg=PA41&dq=model+expansion+cafeobj&source=bl&ots=_vCFynLmca&sig=07V6machOANGM0FTgPF5pcKRrrE&hl=en&ei=YkSgTPn0OoqOjAfb0tWVDQ&sa=X&oi=book_result&ct=result&resnum=1&ved=0CBgQ6AEwAA#v=onepage&q=model%20expansion%20cafeobj&f=false
From what I looked at, their logical notions/terminology are pretty
standard. In general, if you want the class of models to decrease, you
must make the class of theories for them increase (under inclusion
order), and vice-versa.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
