[Haskell-cafe] A model theory question
patrick.browne at dit.ie
Mon Sep 27 03:25:24 EDT 2010
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.
What does the term *forcing* mean?
This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie
More information about the Haskell-Cafe