Re: [isabelle] lattice syntax problems (OR: what does it mean to merge two theories?)



On Sat, Jul 30, 2011 at 2:50 PM, Alexander Krauss <krauss at in.tum.de> wrote:
> On 07/28/2011 09:26 PM, Brian Huffman wrote:
>>
>> But in the short term, it would be nice for theory imports to behave
>> in the way I expect (i.e. actually merge every theory in the import
>> list, without throwing any away).
>
> One cannot change the semantics of theory merges "in the short term", just
> because "no_notation" happens to be conceptually broken. We must get rid of
> it, instead of going further in the same direction.

I am not suggesting that we change the merge behavior "just because
no_notation is broken". Rather, I am suggesting that we change the
merge behavior because the merge behavior itself is broken. The
no_notation command just happens to be the thing that caused me to see
the problem; the basic problem with theory merging is really much more
general.

The current ignore-everything-but-maximal-theories merge behavior was
introduced in 2005:

http://isabelle.in.tum.de/repos/isabelle/rev/f1152f75f6fc

This implementation assumes that when a user imports theories A and B,
where A is an ancestor to B, then merging A and B will always yield a
theory that is identical to B. So, as an optimization, it doesn't
bother to merge A at all.

The implicit assumption here, upon which the correctness of this
optimization rests, is that descendant theories only extend the theory
context in a monotonic fashion. The problem is that this simply is not
true.

The "no_notation" command is one example of something that modifies
the theory context in a non-monotonic way, deleting something from the
context, instead of adding to it. You say that we may eventually get
rid of the "no_notation" command, but what about all the other
commands that delete things from the theory context? Will "declare foo
[simp del]" be phased out as well?

I propose that we go back to the pre-2005 theory merge semantics, by
reverting the relevant portion of changeset f1152f75f6fc. If at some
point in the future we manage to completely eradicate all
non-monotonic theory-updating commands, at that time it might be safe
to reinstate the maximal-theories-only optimization.

- Brian





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