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