[developers] LKB vs. PET divergences

[johnca at sussex.ac.uk]

Quoting Ann Copestake <Ann.Copestake at cl.cam.ac.uk>:

> 
> > There's just not 
> > much freedom to do things differently, or incorrectly.
> 
> I recall a series of cases where we had differences in the past. 
> Anyway, do 
> you have a formal definition anywhere?  The situation is analogous
> to:
> 
> a := top.
> 
> b := top.
> 
> c := top.
> 
> d := a & b & c.
> 
> e := a & b & c.
> 
> where what's happening now in the LKB is that we introduce a glb as
> follows:
> 
> glb := a & b & c.
> 
> d := glb.
> 
> e := glb.
> 
> I am reasonably certain that we discussed this a few years ago and
> agreed this 
> was the preferred behaviour, but I am not sure that I could decide
> for more 
> complex cases.  It'd be nice to have a declarative definition
> somewhere.

I'm not sure how to express this declaratively, but the LKB does the following:

for each type, assign it a code which is the logical OR of its subtypes' codes with one 
additional unique bit set

for every pair of types
  if they have one or more common subtypes (i.e. the logical AND of the type codes is non-
zero)
    but no type currently exists with exactly this code
  then add a newly constructed glb type with this code
iterate this process with any new glb types

insert the newly constructed glb types at approriate points in the type hierarchy, according to 
their codes

For Ann's example:

a := top.
b := top.
c := top.
d := a & b & c.
e := a & b & c.

the types might get the following codes:

e  100000
d  010000
c  111000
b  110100
a  110010
top  111111

and one new glb type would be constructed, with code 110000. This would be inserted into 
the type hierarchy between a,b,c and d,e.

John