Re: [isabelle] antiquotations



On Wed, 13 Feb 2008, Lucas Dixon wrote:

> Alexander Krauss wrote:
> > Since bind_thms is impure, it can only update some global reference
> > hanging around. This is incompatible with paralellism. At the moment it
> > may work sometimes, but it is guaranteed to break sooner or later.
> 
> I'm curious about this: is it really the case that references are
> inherently incompatible with parallelism? Is there some reason why it
> cannot update a thread-local reference?

In principle you can do this, but this requires extra bookeeping of some 
kind of ``thread data environment''.  In post-Isabelle2007 we already have 
this for the "print_mode", which is now thread-safe without giving up the 
slightly odd "setmp" idiom. Such contraptions should be the exeption, not 
the rule.

Even Java programmers have started to envy powerful concepts of purely 
functional programming, which partly explains the current excitement about 
Scala.


> I would expect that you can cut the Isar/ML cake both ways: 
> anti-quotations in Isar or quotations in ML. I feel there should be a 
> confluence proof there somewhere :)

In principle yes.  This is a bit like the Holo Deck in Startrek TNG, which 
is sufficiently powerful to simulate another Enterprise with another fully 
functional Holo Deck inside -- potentially ad infinitum.  In the end it is 
a matter of practical concern which level to take as primary one, which as 
secondary, and stop the nesting at some point.

> So, is there some reason this is not possible? In particular, Isar is 
> executed in ML, so it seems rather strange to me that you cannot 
> replicate it's effect in ML, for example by pasting the function calls 
> used by Isar into the ML.

Since the Isar toplevel is more powerful than the raw ML one, the choice 
of preference is clear to me.  Also you don't want your ``operating 
system'' code (i.e. the Isar infrastructure) pasted into your application 
code.  Moreover, we have recently started to repair some defects in 
versions of SML/ML, by passing through our management of ML sources within 
Isar.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.