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? 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 Thanks, Pat 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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
