1 % (c) 2009-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(kernel_card_arithmetic,[is_inf_or_overflow_card/1, is_finite_card/1,
6 safe_pow2/2, safe_pown/3,
7 safe_add_card/3, blocking_add_card/3,
8 safe_mul/3,
9 safe_minus/3, blocking_factorial/2, blocking_factorial_k/3,
10 choose_nk/3,
11 blocking_nr_iseq/2, blocking_nr_iseq1/2,
12 total_relation_card/3, partial_bijection_card/3,
13 partial_surjection_card/3, total_surjection_card/3,
14 partial_injection_card/3]).
15
16
17 :- use_module(module_information).
18 :- module_info(group,kernel).
19 :- module_info(description,'This module contains cardinality arithmetic that also supports the symbol inf and inf_overflow.'). % in future we may support other ordinals to distinguish countable and uncountable sets
20
21 :- use_module(error_manager).
22 :- use_module(debug).
23 :- use_module(self_check).
24
25 :- assert_must_succeed((safe_pow2(3,R),R==8)).
26 :- assert_must_succeed((safe_pow2(inf,R),R==inf)).
27 :- assert_must_succeed((safe_pow2(inf_overflow,R),R==inf_overflow)).
28 :- assert_must_succeed((safe_pow2(3072,R),R==inf_overflow)).
29 :- assert_must_succeed((safe_pow2(18446744073709551616,R),R==inf_overflow)).
30 :- assert_must_succeed((safe_pow2(500,X), safe_pow2(501,X2), X2 is 2*X)).
31 % :- assert_must_succeed((kernel_objects:safe_pow2(1022,X), kernel_objects:safe_pow2(1023,X2), X2 is 2*X)).
32
33 set_inf_due_to_overflow(Res) :- debug_println(9,'** OVERFLOW (cardinality)**'),Res=inf_overflow.
34 %set_inf_due_to_overflow(Res) :- Res=inf.
35
36 safe_pow2(Exp,Res) :-
37 (Exp==inf -> Res=inf
38 ; Exp==inf_overflow -> Res=inf_overflow
39 ; Exp>1023 /* the limit where SICStus 4.2.1 reported inf; 4.2.3 goes further but uses a huge amount of memory */
40 -> set_inf_due_to_overflow(Res)
41 ; Res is 2^Exp % ^ integer exponentiation operator new in SICStus 4.3
42 ).
43
44 :- assert_must_succeed((safe_pown(3,2,R),R==9)).
45 :- assert_must_succeed((safe_pown(2,3072,R),R==inf_overflow)).
46 :- assert_must_succeed((safe_pown(3,647,R),R==inf_overflow)).
47 :- assert_must_succeed((safe_pown(2,500,X), safe_pown(2,501,X2), X2 is 2*X)).
48 :- assert_must_succeed((safe_pown(2,500,X), safe_pow2(500,X))).
49 :- assert_must_succeed((safe_pown(2,1022,X), safe_pown(2,1023,X2), X2 is 2*X)).
50 :- assert_must_succeed((safe_pown(3,500,X), safe_pown(3,501,X3), X3 is 3*X)).
51 :- assert_must_succeed((safe_pown(inf,2,R),R==inf)).
52 :- assert_must_succeed((safe_pown(inf,inf,R),R==inf)).
53 :- assert_must_succeed((safe_pown(inf_overflow,2,R),R==inf_overflow)).
54 :- assert_must_succeed((safe_pown(2,inf,R),R==inf)).
55 :- assert_must_succeed((safe_pown(2,inf_overflow,R),R==inf_overflow)).
56 :- assert_must_succeed((safe_pown(inf_overflow,inf,R),R==inf)).
57 :- assert_must_succeed((safe_pown(inf_overflow,inf_overflow,R),R==inf_overflow)).
58 safe_pown(Base,Exp,Res) :-
59 ( Base=inf -> (Exp=0 -> Res=1 ; Res=Base)
60 ; Exp=inf -> (Base=0 -> Res=0 ; Base=1 -> Res=1 ; Res=Exp)
61 ; Base=inf_overflow -> (Exp=0 -> Res=1 ; Res=Base)
62 ; Exp=inf_overflow -> (Base=0 -> Res=0 ; Base=1 -> Res=1 ; Res=Exp)
63 ; infinite_pown(Base,Exp) /* SICStus 4.2.1 reported inf; 4.2.3 goes further but uses a huge amount of memory */
64 -> set_inf_due_to_overflow(Res)
65 ; Res is Base ^ Exp % ^ integer exponentiation operator new in SICStus 4.3
66 ).
67
68 /* SICStus 4.2.1 reported inf; 4.2.3 goes further but uses a huge amount of memory */
69 infinite_pown(Base,Exp) :- Exp > 1023, !, Base >= 2.
70 infinite_pown(Base,Exp) :- Exp > 646, !, Base >= 3. % was not really necessary when using overflow_float_pown
71 infinite_pown(Base,Exp) :- Exp > 511, !, Base >= 4.
72 infinite_pown(Base,Exp) :- Exp > 441, !, Base >= 5.
73
74 is_inf_or_overflow_card(inf).
75 is_inf_or_overflow_card(inf_overflow).
76
77 is_finite_card(Card) :- number(Card).
78
79
80 :- assert_must_succeed((safe_mul(3,2,R),R==6)).
81 :- assert_must_succeed((safe_mul(inf,2,R),R==inf)).
82 :- assert_must_succeed((safe_mul(2,inf,R),R==inf)).
83 :- assert_must_succeed((safe_mul(0,inf,R),R==0)).
84 :- assert_must_succeed((safe_mul(inf,0,R),R==0)).
85 % safe_multiplication for positive numbers
86 safe_mul(0,_,R) :- !, R=0. % true for cartesian product: card({}*INTEGER)=0
87 safe_mul(_,0,R) :- !, R=0. % ditto
88 safe_mul(inf,_,R) :- !, R=inf.
89 safe_mul(_,inf,R) :- !, R=inf.
90 safe_mul(inf_overflow,_,R) :- !, R=inf_overflow.
91 safe_mul(_,inf_overflow,R) :- !, R=inf_overflow.
92 safe_mul(X,Y,R) :- is_overflowcheck(R,X*Y).
93
94 :- assert_must_succeed((safe_add_card(3,100,R),R==103)).
95 :- assert_must_succeed((safe_add_card(inf,100,R),R==inf)).
96 :- assert_must_succeed((safe_add_card(inf,inf_overflow,R),R==inf)).
97 :- assert_must_succeed((safe_add_card(inf_overflow,inf,R),R==inf)).
98 :- assert_must_succeed((safe_add_card(inf_overflow,2,R),R==inf_overflow)).
99 safe_add_card(inf,_,R) :- !, R=inf.
100 safe_add_card(_,inf,R) :- !, R=inf.
101 safe_add_card(inf_overflow,_,R) :- !, R=inf_overflow.
102 safe_add_card(_,inf_overflow,R) :- !, R=inf_overflow.
103 ?safe_add_card(X,Y,R) :- is_overflowcheck(R,X+Y).
104
105
106 /* is with overflow check */
107 is_overflowcheck(Var,Expr) :-
108 (Expr=inf -> Var=inf
109 ? ; catch(Var is Expr, error(_,_),
110 set_inf_due_to_overflow(Var)) % optionally add enumeration warning in scope
111 ).
112
113 :- assert_must_succeed((blocking_add_card(3,100,R),R==103)).
114 :- assert_must_succeed((blocking_add_card(inf,100,R),R==inf)).
115 :- assert_must_succeed((blocking_add_card(inf,inf_overflow,R),R==inf)).
116 :- assert_must_succeed((blocking_add_card(inf_overflow,inf,R),R==inf)).
117 :- assert_must_succeed((blocking_add_card(inf_overflow,2,R),R==inf_overflow)).
118
119 % add two cardinalities together: can be number or inf
120 :- block blocking_add_card(-,-,?).
121 blocking_add_card(X,Y,R) :- X==0,!,R=Y.
122 blocking_add_card(X,Y,R) :- Y==0,!,R=X.
123 blocking_add_card(X,_,R) :- X==inf,!,R=inf.
124 blocking_add_card(_,Y,R) :- Y==inf,!,R=inf.
125 ?blocking_add_card(X,Y,R) :- add_card2(X,Y,R).
126
127 :- block add_card2(-,?,?), add_card2(?,-,?).
128 ?add_card2(A,B,R) :- safe_add_card(A,B,R).
129
130
131
132 :- assert_must_succeed((safe_minus(506,501,R),R==5)).
133 :- assert_must_succeed((safe_minus(inf,10,R),R==inf)).
134 :- assert_must_succeed((safe_minus(10,inf,R),R==0)).
135 % subtraction of two positive numbers, supposing first number >= second one
136 :- block safe_minus(-,?,?), safe_minus(?,-,?).
137 safe_minus(_,inf,R) :- !, print('### Warning: cannot compute X - inf'),nl, R=0.
138 safe_minus(inf,_,R) :- !, R=inf.
139 safe_minus(_,inf_overflow,R) :- !, print('### Warning: cannot compute X - inf_overflow'),nl, R=0.
140 safe_minus(inf_overflow,_,R) :- !, R=inf_overflow.
141 safe_minus(X,Y,R) :- R is X-Y.
142
143
144 /*
145 % this code below would sometimes fail in spld generated code:
146 is_overflowcheck_old(Var,Expr) :- print(is_with_overflow(Var,Expr)),nl,
147 (Expr=inf -> Var=inf
148 ; catch(
149 catch(
150 Var is Expr,
151 error(evaluation_error(float_overflow),_),
152 (print(float_overflow),nl,Var = inf)),
153 error(type_error(evaluable,inf/0),_),
154 (print(evaluable_inf),nl,Var=inf))).
155 % catches any exception (e.g. also representation_error when converting inf to integer)
156 % could be unsafe with timeout !!
157 is_errc(Var,Expr) :-
158 (Expr=inf -> Var=inf
159 ; safe_on_exception(_E, Var is Expr, Var = inf)).
160 */
161
162
163
164 :- assert_must_succeed((blocking_factorial(5,R),R==120)).
165 :- assert_must_succeed((blocking_factorial(0,R),R==1)).
166 :- assert_must_succeed((blocking_factorial(1,R),R==1)).
167 :- assert_must_succeed((blocking_factorial(3,R),R==6)).
168 :- assert_must_succeed((blocking_factorial(inf,R),R==inf)).
169 :- block blocking_factorial(-,?).
170 blocking_factorial(inf,R) :- !, R=inf.
171 blocking_factorial(inf_overflow,R) :- !, R=inf_overflow.
172 blocking_factorial(X,R) :- X<0,!, add_error(blocking_factorial,'Negative arg: ',blocking_factorial(X,R)),R=0.
173 blocking_factorial(X,R) :- X>1000,!,
174 % here we overapproximate: throw finite warning in Disprover mode ? or when checking for finite
175 set_inf_due_to_overflow(R).
176 % Note: blocking_safe_pow2(X,R) reports inf for X>1023; for X=171 blocking_factorial gives a result
177 % which is greater than 2**1024 :
178 % X=171,blocking_factorial(X,R),blocking_safe_pow2(1023,R2), R>2*R2.
179 % debug:time(fact(10000,1,_)) --> 170 ms
180 % debug:time(fact(1000,1,_)) --> 0 ms
181 blocking_factorial(A,Res) :- fact(A,1,Res).
182
183 fact(0,Acc,Res) :- !,Res=Acc.
184 fact(N,Acc,Res) :- (is_inf_or_overflow_card(Acc) -> Res=Acc
185 ; safe_mul(N,Acc,NAcc), N1 is N-1, fact(N1,NAcc,Res)).
186
187
188
189 :- assert_must_succeed((blocking_factorial_k(5,5,R),R==120)).
190 :- assert_must_succeed((blocking_factorial_k(5,2,R),R==20)).
191 :- assert_must_succeed((blocking_factorial_k(5,1,R),R==5)).
192 :- assert_must_succeed((blocking_factorial_k(5,0,R),R==1)).
193 :- assert_must_succeed((blocking_factorial_k(5,3,R),R==60)).
194 :- assert_must_succeed((blocking_factorial_k(5,4,R),R==120)).
195 :- assert_must_succeed((blocking_factorial_k(5,6,R),R==0)).
196 :- assert_must_succeed((blocking_factorial_k(0,0,R),R==1)).
197 :- assert_must_succeed((blocking_factorial_k(0,1,R),R==0)).
198 :- assert_must_succeed((blocking_factorial_k(1,1,R),R==1)).
199 :- assert_must_succeed((blocking_factorial_k(2,1,R),R==2)).
200 :- assert_must_succeed((blocking_factorial_k(2,2,R),R==2)).
201 :- assert_must_succeed((blocking_factorial_k(3,3,R),R==6)).
202 :- assert_must_succeed((blocking_factorial_k(inf,1,R),R==inf)).
203 :- assert_must_succeed((blocking_factorial_k(inf,0,R),R==1)).
204 :- assert_must_succeed((blocking_factorial_k(inf,inf,R),R==inf)).
205 :- assert_must_succeed((blocking_factorial_k(2,inf,R),R==0)).
206 % blocking_factorial_k(N,K,Res) :: Res = N*(N-1)*...*(N-K+1)
207 % Number of ways to choose sequences of K different objects amongst a pool of N objects
208 :- block blocking_factorial_k(-,?,?),blocking_factorial_k(?,-,?).
209 blocking_factorial_k(_X,0,R) :- !, R=1.
210 blocking_factorial_k(inf,_,R) :- !, R=inf.
211 blocking_factorial_k(_N,K,R) :- K=inf,!, R=0. % only finitely many _N
212 blocking_factorial_k(inf_overflow,_,R) :- !, R=inf_overflow.
213 blocking_factorial_k(_N,K,R) :- K=inf_overflow,!, R=0.
214 blocking_factorial_k(N,K,R) :- K>N,!, R=0.
215 blocking_factorial_k(A,K,Res) :- fact_k(A,K,1,Res).
216
217 fact_k(0,_,Acc,Res) :- !, Res=Acc.
218 fact_k(_,K,Acc,Res) :- K<1,!,Res=Acc.
219 fact_k(N,K,Acc,Res) :- (is_inf_or_overflow_card(Acc) -> Res=Acc
220 ; safe_mul(N,Acc,NAcc), N1 is N-1, K1 is K-1, fact_k(N1,K1,NAcc,Res)).
221
222
223
224 :- assert_must_succeed((choose_nk(3,3,R),R==1)).
225 :- assert_must_succeed((choose_nk(3,2,R),R==3)).
226 :- assert_must_succeed((choose_nk(3,1,R),R==3)).
227 :- assert_must_succeed((choose_nk(3,0,R),R==1)).
228 :- block choose_nk(-,?,?), choose_nk(?,-,?).
229 choose_nk(N,K,Res) :- (K=0;K=N),!,Res=1.
230 choose_nk(N,K,Res) :- K > N/2,!, KN is N-K, choose_nk2(N,KN,Res).
231 choose_nk(N,K,Res) :- choose_nk2(N,K,Res).
232 choose_nk2(N,K,Res) :- blocking_factorial_k(N,K,NK), blocking_factorial(K,KF),
233 safe_div(NK,KF,Res).
234
235 :- assert_must_succeed((safe_div(inf,10,R),R==inf)).
236 :- assert_must_succeed((safe_div(inf_overflow,10,R),R==inf_overflow)).
237 :- assert_must_succeed((safe_div(inf_overflow,inf,R),R==0)).
238 :- assert_must_succeed((safe_div(inf,inf_overflow,R),R==inf)).
239 :- assert_must_succeed((safe_div(10,inf,R),R==0)).
240 :- assert_must_succeed((safe_div(10,5,R),R==2)).
241 :- assert_must_succeed((safe_div(10,6,R),R==1)).
242 :- block safe_div(-,?,?), safe_div(?,-,?).
243 safe_div(X,0,R) :- print(div_by_zero(X,0,R)),nl, !, R=inf.
244 safe_div(inf,K,R) :-
245 (number(K) -> true ; K=inf_overflow -> true ; print(safe_div(inf,K,R)),nl), !, R=inf.
246 safe_div(_N,inf,R) :- !, R=0.
247 safe_div(inf_overflow,K,R) :-
248 (number(K) -> true ; print(safe_div(inf_overflow,K,R)),nl), !, R=inf_overflow.
249 safe_div(_N,inf_overflow,R) :- !, R=0.
250 safe_div(X,Y,Z) :- Z is X//Y.
251
252
253
254 :- assert_must_succeed((blocking_nr_iseq(2,R),R==5)).
255 :- assert_must_succeed((blocking_nr_iseq(0,R),R==1)).
256 :- assert_must_succeed((blocking_nr_iseq(1,R),R==2)).
257 :- assert_must_succeed((blocking_nr_iseq(3,R),R==16)).
258 :- assert_must_succeed((blocking_nr_iseq(inf,R),R==inf)).
259 :- assert_must_succeed((blocking_nr_iseq(inf_overflow,R),R==inf_overflow)).
260 % number of injective sequences
261 :- block blocking_nr_iseq(-,?).
262 blocking_nr_iseq(inf,R) :- !, R=inf.
263 blocking_nr_iseq(inf_overflow,R) :- !, R=inf_overflow.
264 blocking_nr_iseq(X,R) :- X<0,!, add_error(blocking_nr_iseq,'Negative arg: ',blocking_nr_iseq(X,R)),R=0.
265 blocking_nr_iseq(X,R) :- X>500,!, set_inf_due_to_overflow(R).
266 % Note: blocking_safe_pow2(X,R) reports inf for X>1023; for X=171 blocking_nr_iseq gives a result
267 % which is greater than 2**1024 :
268 % X=171,blocking_nr_iseq(X,R),blocking_safe_pow2(1023,R2), R>2*R2.
269 % debug:time(nr_iseq(10000,_)) --> 250 ms
270 % debug:time(nr_iseq(1000,_)) --> 10 ms
271 % debug:time(nr_iseq(500,_)) --> 0 ms
272 blocking_nr_iseq(A,Res) :- nr_iseq(A,Res). % , print(nr_iseq(A,Res)),nl.
273 % number of injective sequences: f(N) = 1+N*(f(N-1))
274 nr_iseq(0,Res) :- !,Res=1.
275 nr_iseq(N,Res) :- N1 is N-1, nr_iseq(N1,N1Res),
276 safe_mul(N,N1Res,NAcc), safe_add_card(NAcc,1,Res).
277
278 :- assert_must_succeed((blocking_nr_iseq1(2,R),R==4)).
279 :- assert_must_succeed((blocking_nr_iseq1(inf,R),R==inf)).
280 :- assert_must_succeed((blocking_nr_iseq1(inf_overflow,R),R==inf_overflow)).
281 :- public blocking_nr_iseq1/2. % used in card_for_member_closure
282 % number of non-empty injective sequences
283 :- block blocking_nr_iseq1(-,?).
284 blocking_nr_iseq1(inf,R) :- !, R=inf.
285 blocking_nr_iseq1(inf_overflow,R) :- !, R=inf_overflow.
286 blocking_nr_iseq1(A,Res1) :- blocking_nr_iseq(A,Res) , safe_add_card(Res,-1,Res1). %, print(nr_iseq1(A,Res1)),nl.
287
288
289
290 :- assert_must_succeed((total_relation_card(0,inf,R),R==1)).
291 :- assert_must_succeed((total_relation_card(2,inf,R),R==inf)).
292 :- assert_must_succeed((total_relation_card(inf,0,R),R==0)).
293 :- assert_must_succeed((total_relation_card(inf,1,R),R==1)).
294 :- assert_must_succeed((total_relation_card(inf,2,R),R==inf)).
295 :- assert_must_succeed((total_relation_card(inf,inf,R),R==inf)).
296 :- assert_must_succeed((total_relation_card(2,2,R),R==9)).
297 :- assert_must_succeed((total_relation_card(2,3,R),R==49)).
298
299 :- block total_relation_card(-,?,?), total_relation_card(?,-,?).
300 total_relation_card(0,_RanC,Card) :- !, Card=1. % empty set is a solution
301 total_relation_card(_DomC,0,Card) :- !, Card=0. % no element to choose from in the range
302 total_relation_card(inf,RanC,Card) :- !, (RanC=1 -> Card=1 ; Card=inf).
303 total_relation_card(_,inf,Card) :- !, Card=inf.
304 total_relation_card(DomC,RanC,Card) :- safe_pow2(RanC,SubRan),
305 safe_minus(SubRan,1,S1), % as we have a total relation we cannot choose empty set
306 safe_pown(S1,DomC,Card).
307
308
309
310 :- assert_must_succeed((partial_bijection_card(2,inf,R),R==0)).
311 :- assert_must_succeed((partial_bijection_card(inf,2,R),R==inf)).
312 :- assert_must_succeed((partial_bijection_card(inf,inf,R),R==inf)).
313 :- assert_must_succeed((partial_bijection_card(3,2,R),R==6)).
314 :- assert_must_succeed((partial_bijection_card(2,2,R),R==2)).
315 :- assert_must_succeed((partial_bijection_card(1,2,R),R==0)).
316 :- assert_must_succeed((partial_bijection_card(2,1,R),R==2)).
317 :- assert_must_succeed((partial_bijection_card(5,3,R),R==60)).
318 :- assert_must_succeed((partial_bijection_card(6,4,R),R==360)).
319 :- assert_must_succeed((partial_bijection_card(10,1,R),R==10)).
320 :- assert_must_succeed((partial_bijection_card(10,2,R),R==90)).
321
322 :- use_module(inf_arith,[infless/2]).
323
324 :- block partial_bijection_card(-,?,?), partial_bijection_card(?,-,?).
325 partial_bijection_card(_X,0,R) :- !, R=1. % the empty set is a solution
326 partial_bijection_card(inf,X,R) :- !,
327 print_inf_warning(X,'>+>>'), % we could have : INTEGER >+>> POW(INTEGER); TO DO: use omega(inf) for POW ?
328 R=inf. % we know _X>0
329 partial_bijection_card(DomCard,RanCard,Res) :-
330 infless(DomCard,RanCard),!,Res=0. % -> no way to cover all elements in range
331 partial_bijection_card(DomCard,RanCard,XCard) :-
332 choose_nk(DomCard,RanCard,CNK), % ways to choose domain of size RanCard
333 blocking_factorial(RanCard,Card),
334 safe_mul(CNK,Card,XCard).
335
336 print_inf_warning(inf,FUN) :- !, print('### WARNING: Assuming '),
337 print(FUN), print(' exists for two infinite sets'),nl.
338 print_inf_warning(_,_).
339
340
341
342
343 :- assert_must_succeed((partial_surjection_card(0,2,R),R==0)).
344 :- assert_must_succeed((partial_surjection_card(0,0,R),R==1)).
345 :- assert_must_succeed((partial_surjection_card(2,0,R),R==1)).
346 :- assert_must_succeed((partial_surjection_card(1,1,R),R==1)).
347 :- assert_must_succeed((partial_surjection_card(inf,2,R),R==inf)).
348 :- assert_must_succeed((partial_surjection_card(2,inf,R),R==0)).
349 :- assert_must_succeed((partial_surjection_card(inf,inf,R),R==inf)).
350 :- assert_must_succeed((partial_surjection_card(inf_overflow,inf_overflow,R),R==inf_overflow)).
351 :- assert_must_succeed((partial_surjection_card(inf_overflow,10,R),R==inf_overflow)).
352 :- assert_must_succeed((partial_surjection_card(3,2,R),R==12)).
353 :- block partial_surjection_card(-,?,?), partial_surjection_card(?,-,?).
354 partial_surjection_card(_X,0,R) :- !, R=1. % the empty set is a solution
355 partial_surjection_card(inf,X,R) :- !,print_inf_warning(X,'+->>'),R=inf. % we know _X>0
356 partial_surjection_card(DomCard,RanCard,R) :-
357 infless(DomCard,RanCard), !, R=0. % -> no way to cover all elements in range
358 partial_surjection_card(inf_overflow,_,R) :- !, R=inf_overflow.
359 partial_surjection_card(A,B,Res) :- tsurjcard(A,1,B,Res). % 1 because we can choose to leave the function undefined
360
361 :- assert_must_succeed((total_surjection_card(0,2,R),R==0)).
362 :- assert_must_succeed((total_surjection_card(0,0,R),R==1)).
363 :- assert_must_succeed((total_surjection_card(2,0,R),R==0)).
364 :- assert_must_succeed((total_surjection_card(inf,0,R),R==0)).
365 :- assert_must_succeed((total_surjection_card(inf,1,R),R==1)).
366 :- assert_must_succeed((total_surjection_card(inf,2,R),R==inf)).
367 :- assert_must_succeed((total_surjection_card(2,inf,R),R==0)).
368 :- assert_must_succeed((total_surjection_card(0,inf,R),R==0)).
369 :- assert_must_succeed((total_surjection_card(inf,inf,R),R==inf)).
370 :- assert_must_succeed((total_surjection_card(inf,inf_overflow,R),R==inf)).
371 :- assert_must_succeed((total_surjection_card(inf_overflow,inf_overflow,R),R==inf_overflow)).
372 :- assert_must_succeed((total_surjection_card(inf_overflow,100,R),R==inf_overflow)).
373 :- assert_must_succeed((total_surjection_card(inf_overflow,inf,R),R==0)).
374 :- assert_must_succeed((total_surjection_card(3,2,R),R==6)).
375 :- block total_surjection_card(-,?,?), total_surjection_card(?,-,?).
376 total_surjection_card(0,Range,R) :- !,(Range=0 -> R=1 % the empty set is a solution
377 ; R=0). % no solution
378 total_surjection_card(_X,0,R) :- !, R=0. % as _X>0 there is no way to construct a total function
379 total_surjection_card(_X,1,R) :- !, R=1. % we only have one choice for every element of _X
380 total_surjection_card(inf,X,R) :- !,print_inf_warning(X,'-->>'),R=inf. % we know _X>0
381 total_surjection_card(DomCard,RanCard,R) :-
382 infless(DomCard,RanCard), !, R=0. % -> no way to cover all elements in range, applicable if RanCard=inf
383 total_surjection_card(inf_overflow,_,R) :- !, R=inf_overflow.
384 total_surjection_card(A,B,Res) :- tsurjcard(A,0,B,Res).
385
386 tsurjcard(Rem,_AlreadyUsed,StillToBeUsed,Res) :- Rem<StillToBeUsed,!,Res=0. % no solution
387 tsurjcard(0,_AlreadyUsed,_StillToBeUsed,Res) :- !, Res=1. % we have finished
388 tsurjcard(Rem,AlreadyUsed,StillToBeUsed,Res) :-
389 R1 is Rem-1, A1 is AlreadyUsed+1, S1 is StillToBeUsed-1,
390 (AlreadyUsed=0 -> ResA=0 ; tsurjcard(R1,AlreadyUsed,StillToBeUsed,ResA)),
391 (StillToBeUsed=0 -> ResB =0 ; tsurjcard(R1,A1,S1,ResB)),
392 Res is AlreadyUsed*ResA+StillToBeUsed*ResB.
393
394
395
396 :- assert_must_succeed((partial_injection_card(1,1,R),R==2)).
397 :- assert_must_succeed((partial_injection_card(1,2,R),R==3)).
398 :- assert_must_succeed((partial_injection_card(1,100,R),R==101)).
399 :- assert_must_succeed((partial_injection_card(0,100,R),R==1)).
400 :- assert_must_succeed((partial_injection_card(1,inf,R),R==inf)).
401 :- assert_must_succeed((partial_injection_card(0,inf,R),R==1)).
402 :- assert_must_succeed((partial_injection_card(5,0,R),R==1)).
403 :- assert_must_succeed((partial_injection_card(inf,0,R),R==1)).
404 :- assert_must_succeed((partial_injection_card(inf,1,R),R==inf)).
405 :- assert_must_succeed((partial_injection_card(5,1,R),R==6)).
406
407 :- block partial_injection_card(-,?,?), partial_injection_card(?,-,?).
408 partial_injection_card(Dom,Ran,R) :- (Dom=0;Ran=0),!, R=1. % only one solution: empty function
409 partial_injection_card(Dom,1,R) :- !,
410 (Dom=inf -> R=inf ; Dom=inf_overflow -> R=inf_overflow
411 ; R is Dom+1). % empty function + for every domain element one function
412 partial_injection_card(inf,inf,Card) :- !, print_inf_warning(inf,'>+>'), Card=inf.
413 partial_injection_card(inf_overflow,inf_overflow,Card) :- !, print_inf_overflow_warning('>+>'), Card=inf_overflow.
414 partial_injection_card(Dom,Ran,R) :- (Dom=inf;Ran=inf),!, R=inf.
415 partial_injection_card(Dom,Ran,R) :- (Dom=inf_overflow;Ran=inf_overflow),!, R=inf_overflow.
416 partial_injection_card(Dom,Ran,R) :- Dom>1000,Ran>1000,!, set_inf_due_to_overflow(R). % TO DO: refine this
417 % would give a result larger than blocking_factorial(1000)
418 partial_injection_card(DCard,RCard,Card) :-
419 pinj_card(1,DCard,RCard,1,Card).
420
421 % TO DO: can we compute this directly rather than using recursion ?
422 pinj_card(I,M,N,Acc,Res) :- (I>M ; I>N ; Acc=inf),!, Res=Acc.
423 pinj_card(I,M,N,Acc,Res) :-
424 choose_nk(M,I,MI), % ways to choose domain of size I
425 blocking_factorial_k(N,I,NI), % ways to map the domain of size I to N
426 safe_mul(MI,NI,MINI), safe_add_card(MINI,Acc,NewAcc),
427 I1 is I+1, pinj_card(I1,M,N,NewAcc,Res).
428
429 :- public total_bijection_card/3. % exported in is_a_relation above
430 :- block total_bijection_card(-,?,?), total_bijection_card(?,-,?).
431 total_bijection_card(inf,inf,Card) :- !, print_inf_warning(inf,'>->>'), Card=inf.
432 total_bijection_card(inf_overflow,inf_overflow,Card) :- !, print_inf_overflow_warning('>->>'), Card=inf_overflow.
433 total_bijection_card(DCard,RCard,Card) :- DCard \= RCard,!,Card=0.
434 total_bijection_card(RCard,RCard,Card) :- blocking_factorial(RCard,Card).
435
436
437 print_inf_overflow_warning(FUN) :- !, print('### WARNING: Assuming '),
438 print(FUN), print(' exists for two very large sets sets'),nl.
439 % TODO: probably produce enumeration_warning or virtual time-out or similar