mod CLIMBING is
    protecting INT .
    protecting QID .
    protecting STRING .
    
        sort Rel .
	
	sorts NamePair .
	sorts Parent Sibling Cousin RelType .
	subsorts Parent Sibling Cousin < RelType .

	op Parent : Nat -> Parent .
	op Cousin : Nat Nat -> Cousin .
	op Sibling : -> Sibling .

	op pair : Qid Qid -> NamePair .
	op rel : NamePair RelType -> Rel . 
	op parent : Qid Qid -> Rel .

	op Empty : -> Rel [ ctor ] .
	op __ : Rel Rel -> Rel [ ctor assoc comm id: Empty ] .

	op init : -> Rel .
	eq init =
parent('alonzo.church, 'oswald.veblen) 
parent('stephen.kleene, 'alonzo.church) 
parent('dana.scott, 'alonzo.church) 
parent('martin.davis, 'alonzo.church) 
parent('pat.fischer, 'hartley.rogers) 
parent('mike.paterson, 'david.park) 
parent('dennis.ritchie, 'pat.fischer) 
parent('hartley.rogers, 'alonzo.church) 
parent('les.valiant, 'mike.paterson) 
parent('bob.constable, 'stephen.kleene) 
parent('david.park, 'hartley.rogers) .


	vars A B : Qid .
	vars X Y Z : Qid .

	vars N M O P : Nat .
	vars R : RelType .
	vars REST : Rel .


---- Note that the input is in (child, parent) format, but we want to output (parent, child)

	rl [ parent ] : parent(A, B) => rel( pair(B, A), Parent(0)) .

	rl [ grandparent ] : 
	     		 rel( pair(X, Y), Parent(0))
			 rel( pair(Y, Z), Parent(N)) => rel( pair(X, Z), Parent(N + 1)) .

---- sibling is reflexive

	rl [ sibling ] : 
	     		 rel( pair(X, Y), Parent(0))
			 rel( pair(X, Z), Parent(0)) => rel( pair(Y, Z), Sibling) rel( pair(Z, Y), Sibling) .

---- check least ancestor
	rl [ cousin ] :
			 rel( pair(X, Y), Parent(N))
			 rel( pair(X, Z), Parent(M)) => rel( pair(Y, Z), Cousin(min(N,M), abs(N - M))) .
endm

search [1] in CLIMBING : init =>+ rel (pair ('stephen.kleene, 'bob.constable), R) REST .
search [1] in CLIMBING : init =>+ rel (pair ('hartley.rogers, 'stephen.kleene), R) REST .

----- search [1] in CLIMBING : init =>+ rel (pair ('les.valiant, 'alonzo.church), R) REST .
----- swap this query to search for father instead of child

search [1] in CLIMBING : init =>+ rel (pair ('alonzo.church, 'les.valiant), R) REST .

search [1] in CLIMBING : init =>+ rel (pair ('les.valiant, 'dennis.ritchie), R) REST .
search [1] in CLIMBING : init =>+ rel (pair ('dennis.ritchie, 'les.valiant), R) REST .
search [1] in CLIMBING : init =>+ rel (pair ('pat.fischer, 'michael.rabin), R) REST .

quit