156 Examples of correspondence between Predica and logic

The following table provides examples of queries expressed in Predica and shows how they correspond to logic-frame denotations. The right-hand column uses the short display form of a frame, omitting the free-variable set when it is clear from the result and formula:

Predica Logic-frame display 

            s.supplier
        
supplier=S:Supplier
where
  s.supplier(S)
 

            s.supplier.[city="London"]
        
supplier=S:Supplier
where
  s.supplier(S)
  ∧ ∃C:String
    S.city(C)
    ∧ C = "London"
 

            s.supplier.[city="London"].name
        
name=N:String
where
  ∃S:Supplier ∃C:String
    s.supplier(S)
  ∧ S.city(C)
  ∧ C = "London"
  ∧ S.name(N)
 

        s.shipment.(
            supplier.name as sname, 
            part.name as pname, 
            qty)
        
sname=SN:String, 
pname=PN:String, 
qty=Q:Integer
where
  ∃SP:Shipment ∃S:Supplier ∃P:Part
    s.shipment(SP)
  ∧ SP.supplier(S)
  ∧ S.name(SN)
  ∧ SP.part(P)
  ∧ P.name(PN)
  ∧ SP.qty(Q)
 

        s.supplier.(
            name as sname,
            shipment.(part.name as pname, qty))
        
sname=SN:String, 
pname=PN:String, 
qty=Q:Integer
where
  ∃S:Supplier ∃SP:Shipment ∃P:Part
    s.supplier(S)
  ∧ S.name(SN)
  ∧ S.shipment(SP)
  ∧ SP.part(P)
  ∧ P.name(PN)
  ∧ SP.qty(Q)
 

        s.supplier.[shipment.Σexists]
        
supplier=S:Supplier
where
  s.supplier(S)
  ∧ ∃SP:Shipment
    S.shipment(SP)
Suppliers that don't ship any parts (anti-join) 

        s.supplier.[shipment.Σempty]
        
supplier=S:Supplier
where
  s.supplier(S)
  ∧ ¬∃SP:Shipment
    S.shipment(SP)
suppliers where all parts they ship are red 

        s.supplier.[shipment.part.color.Σ ⊆ {Color.red}]
        
supplier=S:Supplier
where
  s.supplier(S)
  ∧ { C:Color | ∃SP:Shipment ∃P:Part
      S.shipment(SP)
      ∧ SP.part(P)
      ∧ P.color(C) } ⊆ {Color.red}
 

            s.supplier.[city="London"].(name,status)
Alternatively 

            s.supplier.[city="London"].(name ⊓ status)
        
name=N:String, 
status=T:Integer
where
  ∃S:Supplier ∃C:String
    s.supplier(S)
  ∧ S.city(C)
  ∧ C = "London"
  ∧ S.name(N)
  ∧ S.status(T)
 

            s.supplier.[city="London"].(name ⊔ status)
        
name=N:String, 
status=T:Integer
where
  ∃S:Supplier ∃C:String
    s.supplier(S)
  ∧ S.city(C)
  ∧ C = "London"
  ∧ (
    S.name(N)
    ∨ S.status(T)
  )
 

            s.supplier.[city="London"].(name, status!)
        
name=N:String, 
status=T:Integer
where
  ∃S:Supplier ∃C:String
    s.supplier(S)
  ∧ S.city(C)
  ∧ C = "London"
  ∧ S.name(N)
  ∧ ¬S.status(T)
  • s.supplier.city ⊔ s.part.city
  • s.supplier.city ∪ s.part.city
  • s.(supplier.city ⊔ part.city)
  • s.(supplier.city ∪ part.city) 
city=C:String
where
  (∃S:Supplier
    s.supplier(S)
    ∧ S.city(C))
  ∨ (∃P:Part
    s.part(P)
    ∧ P.city(C))
 

            s.(  supplier.name
               ⊔ part.[color=Color.red].name)
        
name=N:String
where
  (∃S:Supplier
    s.supplier(S)
    ∧ S.name(N))
  ∨ (∃P:Part
    s.part(P)
    ∧ P.color(Color.red)
    ∧ P.name(N))
 

            s.(  supplier.(name, city)
               ⊔ part.(name, city) )
        
name=N:String, 
city=C:String
where
  (∃S:Supplier
    s.supplier(S)
    ∧ S.name(N)
    ∧ S.city(C))
  ∨ (∃P:Part
    s.part(P)
    ∧ P.name(N)
    ∧ P.city(C))
 

        s.supplier.[shipment.Σ = ∅]
      
supplier=S:Supplier
where
  s.supplier(S)
  ∧ {SP:Shipment | S.shipment(SP)}=∅
 

        s.supplier -- s.shipment.supplier
      
supplier=S:Supplier
where
  s.supplier(S)
  ∧ ¬(
    ∃SP:Shipment
      s.shipment(SP)
      ∧ SP.supplier(S)
  )
 

        s.part⇒(shipment.supplier)
      
supplier=S:Supplier
where
  ∀P:Part
    s.part(P)
    → ∃SP:Shipment
      P.shipment(SP)
      ∧ SP.supplier(S)
 

        s.supplier.[shipment.part.Σ = s.part.Σ]
      
supplier=S:Supplier
where
  s.supplier(S)
  ∧ { P:Part | ∃SP:Shipment
      S.shipment(SP)
      ∧ SP.part(P) }
    = { P:Part | s.part(P) }