Computing the core of a distributed system

Input: A dstributed systems consisting of a list of classifications, a list of informorphisms, and a list of constraints.

Output: A universal cover (= core) of the input distributed system.

Remark(1): The cover computed by this cgi is not exactly universal; the intermediate arrow to other covers always does exist but not necessarily unique. However this is not a problem in theory and practice.

Remark(2): 'Atoms' of each classfication are represented by 'sequents' of types due to adjointness of informorphism. Thanks to this fact, the token maps are replaced with that on these atoms, which has made also the algorithm much simpler.

A term

	 cla([x,y],[a],[a-[x,y]]),cla([x,y],[a],[a-[x,y]])

means a classification whose

	token set is  [x,y] ,
	type set is  [a] ,
	with support relation  [a-[x,y]]

which reads

	x  supports  a, and
	y  supports  a.

A term

	 [cla([x,y],[a],[a-[x,y]]),cla([x,y],[a],[a-[x,y]])]

means a list of two classfications,

	 cla([x,y],[a],[a-[x,y]]) , and
	 cla([x,y],[a],[a-[x,y]]) ,

which are indexed 1 and 2 in order. Note that, in this case, the two classifications are identical as a classification, but are indexed differently, which is necessary for sum operations.

A term

	 im(1,2, [a-a],[x-x])

means an informorphism from the classification 1 to the classification 2, whose

	token map is [x-x] (identity) and
	type map is [a-a] (identity).

A sequent [1:a, 2:b]-[3:c] means the set of tokens which supports

	type  1:a ,
	and  2:b ,
	but not  3:c ,

where 1,2,3 are indexes of classifications.

The term, [[[a]-[],[a]-[]]] appearing in the output token area means the set of tokens as a list [u, v] such that

	u supports a (in classification 1),
and
	v supports a (in classification 2).

In other words, the tokens set of the core is represented as an idexed sequence of sequents with the same idexing set for given series of classifications.

The term,

	 [[1:b,1:a,2:a]]

appearing in the output type area means the set of types. In this particular case the set is a singleton of the sum type

	 [1:b, 1:a, 2:a] .

It is straightforward to recover the token set and the support relation from this conventional representation, which is the reason why neither tokens nor support relation of the core built appear in the output area,