[Haskell-cafe] A model theory question

[Alexander Solla]

  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.