example FOAF

#  CQL + EDs is equivalent to Evan Patterson's "relational ologs".  Going to the latter from the former is trivial.
# 
#  The algorithm for translating a relational olog to CQL + EDs involves structural recursion on formulae,
#  so here is just an example instead.
#
#  Look at Section 8 of the relational ologs paper.  Each relational olog is equivalent to a bunch of n-ary relation symbols
#  and formulae in "regular logic" (i.e., each operator in table 2 can be defined as a formula in regular logic).  
#  Then, each n-ary relation symbol turns into an n-way CQL span, and each formula in regular logic:
#
#    forall xs. (exists ys. phi(xs,ys)) -> (exists ys. psi(xs, ys))
#
#  is equivalent to an ED by virtue of "classical logic" (which holds in the category of Sets):
#
#    forall xs ys. phi(xs,ys) -> exists ys'. psi(xs, ys’)
#
# The CQL file below does a bunch of the "friend of a friend" example from Evan's section 8 using the above translation.



typeside Ty = literal {
	types
		Number
		String
}

schema FOAF = literal : Ty {
	entities
		#entities
		Person
		Organization
		#spans
		knows
		friend_of
		works_at
		salary
		enemy_of
		frenemy_of
	foreign_keys #total functions
		knows1 : knows -> Person
		knows2 : knows -> Person
		friend_of1 : friend_of -> Person
		friend_of2 : friend_of -> Person
		works_at1 : works_at -> Person
		works_at2 : works_at -> Organization
		salary1 : salary -> Person
		salary2 : salary -> Organization
		enemy_of1 : enemy_of -> Person
		enemy_of2 : enemy_of -> Person
		frenemy_of1 : frenemy_of -> Person
		frenemy_of2 : frenemy_of -> Person
	attributes #total functions
		family_name : Person -> String
		age : Person -> Number	
		given_name : Person -> String
		salary3 : salary -> Number
}

constraints knows_symmetric = literal : FOAF {
forall k1:knows -> 
exists k2:knows 
where k1.knows1 = k2.knows2
     k1.knows2 = k2.knows1	
}

#x:person y:organization | exists z:number salary(x,y,z) -> works_at(x,y)
#equivalent, classically etc to
#x:person y:organization z:number | salary(x,y,z) -> works_at(x,y)
constraints works_at_determined1 = literal : FOAF {
forall s:salary ->
exists w:works_at 
where s.salary1 = w.works_at1
     s.salary2 = w.works_at2
}

#x:person y:organization | works_at(x,y) -> exists z:number salary(x,y,z) 
constraints works_at_determined2 = literal : FOAF {
forall w:works_at ->
exists s:salary 
where s.salary1 = w.works_at1
     s.salary2 = w.works_at2
}

#frenemy_of is intersection of friend_of and enemy_of
constraints frenemy_determined = literal : FOAF {
forall fr : frenemy_of ->
exists f : friend_of
      e : enemy_of
where fr.frenemy_of1 = f.friend_of1
     fr.frenemy_of2 = f.friend_of2
     fr.frenemy_of1 = e.enemy_of1
     fr.frenemy_of2 = e.enemy_of2
}