Hyper Effect Algebras

Definition: A partial binary hyper operation on A is a partial mapping from A×A into P(A)^*, where P(A)^* is the set of all non-empty subsets of A.

We say that A + B is defined, iff for any a ∈ A and b ∈ B is a + b defined.

We say that A + a is defined, iff A + {a} is defined.

Definition: The set A equipped with partial hyper operation +, unary operation ' and constants 0, 1 is said to be hyper effect algebra, if the following properties are satisfied:

Operation + is partially commutative, i.e. x + y is defined, iff y + x is defined and in such case x + y = y + x.
Operation + is partially associative, i.e. x + y is defined and (x + y) + z is defined, iff y + z is defined and x + (y + z) is defined and in such case (x + y) + z = x + (y + z).
For any x∈A there is a unique y∈A such that 1∈x + y.
x + 0 is defined for any x in A.
1 + x is defined, iff x = 0.
Relation ≤ defined as: (x≤y, iff x + y' is defined) is reflexive and antisymmetric

If moreover ≤ is transitive, we say that A is a transitive hyper effect algebra..

Finite models

n = 1

Case no.	# models	# models non iso
1	1

n = 2

Case no.	# models	# models non iso
1	2

n = 3

Rel	Case no.	# models generated	# models non iso	tested possibilities	single core time est.	tested possib. new	new sg. core time est.
1	1	17		28	<1s	17	<1s

* k, M, G are iso prefixes 10³, 10⁶, 10⁹, respectfully.

n = 4

Rel	Case no.	# models generated	# models non iso	tested possibilities	single core time est.	tested possib. new	new sg. core time est.
1	1	345	186	1 600	<1s	345	<1s
1	2	61	38	200	<1s	61	<1s
2	3	276		1 280	<1s	342	<1s
Total		682	500	3 080	<1s	748	<1s

* k, M, G are iso prefixes 10³, 10⁶, 10⁹, respectfully.

Data summary: 4.csv

n = 5

Rel	Case no.	# models generated	# models non iso	tested possibilities	single core time est.	tested possib. new	new sg. core time est.
1	1	22 139	4 005	372 736	5s	22 139	2s
1	2	2 071	1 195	23 296	<1s	2 071	<1s
2	3	20 374		445 440	4s	28 048	2s
3	4	6 494		371 200	4s	9 250	<1s
4	5	32 061		10 967 040	2m 8s	415 655	17s
5	6	10 718		2 795 520	32s	10 718	1s

* k, M, G are iso prefixes 10³, 10⁶, 10⁹, respectfully.

Data summary: 5.csv

n = 6

Rel	Case no.	# models generated	# models non iso	tested possibilities	single core time est.	tested possib. new	new sg. core time est.
1	1	5 344 185	233 753	5 344 185	9m 38s	5 344 185	12m 1s
	2	239 585	66 360	239 585	31s	239 585	35s
	3	12 425	2 118	21 781	1s	12 425	2s
2	4	4 862 062	2 451 083	10 651 416	12m 8s	7 034 396	13m 26s
2	5	270 368	145 994	1 120 152	53s	397 570	47s
3	6	2 777 965		9 585 740	8m 50s	4 153 092	7m 59s
4	7	46 314 262		1 171 001 260	8h 5m 48s	227 651 318	3h 46m 40s
5	8	31 144 212		112 125 780	1h 49m 37s	31 144 212	1h 20m 45s
6	9	195 671	98 331	910 530	40s	424 062	40s
6	10	4 744 466	2 373 963	24 255 660	17m 14s	9 087 940	15m 37s
7	11	2 276 152		48 547 928	21m 12s	11 583 892	12m 47s
8	12	1 909 068		7 625 376	5m 52s	2 629 184	5m 46s
9	13	16 905 421	8 457 557	2 501 293 288	14h 8m 5s	274 647 724	3h 54m 58s
10	14	14 522 672		230 802 240	1h 38m 5s	46 312 336	1h 5m 11s
11	15	13 219 304	6 623 143	65 182 412	47m 35s	19 894 826	34m 31s
11	16	694 686	354 682	3 553 220	2m 40s	1 069 332	2m 17s
12	17	4 861 691		97 330 272	53m 12s	23 462 188	29m 52s
13	18	63 271 944	31 683 225	153 334 400	3h 18m 52s	63 271 944	3h 9m 38s
13	19	3 275 582	1 663 306	7 952 000	11m 13s	3 275 582	10m 13s
14	20^***	0		-	-	-	-
14	21^***	0		-	-	-	-
15	22	19 739 376	9 874 263	46 958 660	56m 25s	19 739 376	44m 54s
15	23	18 650 704	9 330 836	44 531 200	53m 4s	18 650 704	45m 5s
16	24	146 622 918		2 453 008 200	19h 50m 9s	452 575 620	9h 50m 22s
17	25	8 739 167		6 310 906 880	1d 2h 50m 1s	191 352 386^**	3h 3m 4s
18	26	16 044 184		188 636 160	1h 47m 3s	52 925 236	1h 19m 12s

* k, M, G are iso prefixes 10³, 10⁶, 10⁹, respectfully.

** Special elimination for the linear case.
[ a + a ⊆ {0, a, b}, b∈ a + a; a + b ⊆ {0, a, b, c}, c∈ a + b; d∈ a + c; d∈ b + b ]

*** Proved that there are no models.

Data summary: 6.csv

Source code: hyperEA_src.tar.xz (167.4 kB)

Additional files: