53 Isomorphisms

Predica supports declarations of isomorphisms between types.

Example: isomorphism between optional and variant

value A
{
    T v?;
}

variant B
{
    T v;
    Boolean unknown;
}

A a ← B b
{
    a.v = if b.unknown then none else b.v;
}

B b ← A a
{
    b = if a.v = none then unknown(true) else v(a.v);
}

Example: isomorphism with separation into known and unknown

namespace A
{
    @domain("employee with known name")
    entity R1 
    {
        Integer id;
        String name;
        key {id};
    }

    @domain("employee with known address")
    entity R2 
    {
        Integer id;
        String address;
        key {id};
    }

    entity System
    {
        R1 r1*;
        R2 r2*;
        → all* = r1 ∪ r2;
    }
}

namespace B
{
    @domain("employee with known name and unknown address")
    entity S1 
    {
        Integer id;
        String name;
        key {id};
    }

    @domain("employee with known address and unknown name")
    entity S2 
    {
        Integer id;
        String address;
        key {id};
    }

    @domain("employee with known name and known address")
    entity S3 
    {
        Integer id;
        String name;
        String address;
        key {id};
    }

    entity System
    {
        S1 s1*;
        S2 s2*;
        S3 s3*;
        → all* = s1 ∪ s2 ∪ s3;
        constraints
        {
            disjoint { s1, s2, s3 };
        }
        theorems
        {
            // Employees with both name and address known
            s3 = (s1 ∪ s3) ∩ (s2 ∪ s3);

            // These follow from the disjointness axiom
            s1 ∩ s2 = ∅;
            s1 ∩ s3 = ∅;
            s2 ∩ s3 = ∅;
        }
    }
}

isomorphism employeeInfoRefinement
{
    // {R1, R2} → {S1, S2, S3}
    a:A.System → B.System   
    {
        s3 = a.r1 ⨝ a.r2;
        s1 = a.r1 ∖ s3.{id, name};
        s2 = a.r2 ∖ s3.{id, address};
    }

    // {S1, S2, S3} → {R1, R2}
    b:B.System → A.System
    {
        r1 = b.s1 ∪ b.s3.{id, name};
        r2 = b.s2 ∪ b.s3.{id, address};
    }
}

A has two prime factors and B has one. So for updating A is superior. B is more useful for read-only views. The bijection is nice to know because B is non-lossy.

Attribute predicates as unary relations

In the above example there is an expression s1 ∪ s2 ∪ s3.

entity System
{
    S1 s1*;
    S2 s2*;
    S3 s3*;
    → all* = s1 ∪ s2 ∪ s3;
}

At first glance, the expression s1 ∪ s2 ∪ s3 may appear ill-formed when viewed through the lens of traditional Relational Algebra where this is taking the union of relvars which are not union compatible.

In Predica, however, each attribute, whether declared or derived, is a unary predicate. Its extension is simply the set of entity instances for which the attribute holds. Set-theoretic operations such as union, intersection, and difference therefore apply directly to attributes, irrespective of the internal structure or declared type of the associated entities. These operations are performed over their unary extensions, not over multi-attribute relational schemas.

Example: internal isomorphisms

The problem with the above isomorphism approach is that it doesn't actually give rise to a single type that simultaneously enjoys both representations. But that is desirable because it means you can read or update using either representation.

value Point
{
    // cartesian representation
    Real x;
    Real y;

    // polar representation
    Real r where r ≥ 0;
    Real θ where 0 ≤ θ < 2*pi;

    constraints
    {
        r=0 → θ=0;
    }

    isomorphism {x,y} ↔ {r,θ}
    {
        r = sqrt(x^2 + y^2);
        θ = atan2(y,x);
        x = r * cos θ;
        y = r * sin θ;
    }
}