• API
• FAQ
• Tools
• Archive
SHARE
TWEET

stoopkid

a guest Nov 19th, 2019 100 in 10 days
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. %
2.
3. fin(N,0) :- N > 0.
4. fin(SN,SX) :- SN > 1, N is SN - 1, fin(N, X), SX is X + 1.
5.
6. /*
7. fin(N,X) :-
8.     0 =< X,
9.     X < N.
10. */
11.
12. succ(X, Y) :-
13.     Y is X + 1.
14.
15. % enumerability property:
16. /*
17. a relation R/n is enumerable if for every vector v = <x_1, ..., x_n> of terms,
18. such that Rv, then v is in the solution set of RV where V is the vector <X_1, ..., X_n> of variables.
19.
20.
21. */
22.
23.
24. l1(0,"h").
25. l1(1,"e").
26. l1(2,"l").
27. l1(3,"l").
28. l1(4,"o").
29. l1(5," ").
30. l1(6,"w").
31. l1(7,"o").
32. l1(8,"r").
33. l1(9,"l").
34. l1(10,"d").
35. l1(11,".").
36.
37. l2(0,1).
38. l2(1,0).
39. l2(2,1).
40. l2(3,0).
41. l2(4,1).
42.
43. l3(0,1).
44. l3(1,0).
45. l3(2,1).
46.
47. l4(0,1).
48. l4(1,0).
49. l4(2,1).
50.
51. l5(0,0).
52. l5(1,0).
53. l5(2,0).
54. l5(3,1).
55. l5(4,0).
56. l5(5,1).
57. l5(6,2).
58. l5(7,2).
59. l5(8,2).
60. l5(9,1).
61. l5(10,0).
62. l5(11,1).
63. l5(12,4).
64. l5(13,4).
65. l5(14,4).
66.
67. s(1).
68. s(2).
69. s(3).
70.
71. t(1).
72. t(2).
73. t(4).
74. t(5).
75.
76. r(1,1).
77. r(1,2).
78. r(2,1).
79. r(2,3).
80.
81. oh1(0,2).
82. oh1(1,3).
83. oh1(2,4).
84.
85. /*
86. % needs to know domain in order to be enumerable
87. complement(S, X) :- \+ call(S, X).
88.
89. % but then this is just difference(A,S)...
90. complement2(S, X) :- domain(S, A), call(A,  X), \+ call(S, X).
91. */
92.
93. % enumerable whenever S1 and S2 are enumerable
94. intersection(S1, S2, X) :- call(S1, X), call(S2, X).
95.
96. % enumerable whenever S1 and S2 are enumerable
97. union(S1, S2, X) :- call(S1, X) ; (call(S2, X), \+call(S1, X)).
98.
99. % doesn't filter repeats
100. disjoint_union(S1, S2, X) :- call(S1, X) ; call(S2, X).
101.
102. % creates different objects for repeats, making it an actual disjoint union
103. % enumerable whenever S1 and S2 are enumerable
104. disjoint_union2(S1, _, left(X)) :- call(S1, X).
105. disjoint_union2(_, S2, right(X)) :- call(S2, X).
106.
107. % enumerable whenever S1 and S2 are enumerable
108. cartesian_product(S1, S2, (X, Y)) :- call(S1, X), call(S2, Y).
109.
110. first((X, _), X).
111. second((_, Y), Y).
112.
113.
114. % difference(S1,S2) is intersection of S1 with complement of S2
115. % enumerable whenever S1 and S2 are enumerable
116. difference(S1, S2, X) :- call(S1, X), \+ call(S2, X).
117.
118. % this won't actually retrieve the intersection, i.e. you can't call it with variable X and return all elements of the intersection
119. /*
120. intersection_set(S, X) :-
121.     \+ ((
122.         call(S, Set2),
123.         \+ call(Set2, X)
124.     )).
125. */
126.
127. % this will retrieve the intersection, but the results will be duplicated
128. /*
129. intersection_set(S, X) :-
130.     call(S, Set),
131.     call(Set, X),
132.     \+ ((
133.         call(S, Set2),
134.         \+ call(Set2, X)
135.     )).
136. */
137.
138. % this will retrieve the intersection and prevent duplication
139. /*
140. intersection_set(S, X) :-
141.     % if the objects in the intersection are in every set in S,
142.     % then we can pick any single set in S and use that to generate all the elements of the intersection
143.     % whatever set Set we pick, the elements of the intersection must be in Set
144.     call(S, Set),
145.     !,
146.     call(Set, X),
147.     \+ ((
148.         call(S, Set2),
149.         \+ call(Set2, X)
150.     )).
151. */
152.
153. % this won't retrieve the intersection
154. /*
155. intersection_set(S, X) :-
156.     forall(S, [Set]>>(call(Set,X))).
157. */
158.
159. % this will retrieve the intersection and prevent duplication
160. % is it a hack? idk
161. % enumerable whenever S is enumerable and forall Set in S, Set is enumerable
162. intersection_set(S, X) :-
163.     call(S, Set),
164.     !,
165.     call(Set, X),
166.     forall(S, [Set2]>>(call(Set2,X))).
167.
168.
169. % closer to disjoint union; doesn't filter repeats
170. union_set(S, X) :-
171.     call(S, Set),
172.     call(Set, X).
173.
174. disjoint(S1, S2) :- \+ intersection(S1, S2, _).
175.
176. disjoint_set(S) :-
177.     \+((
178.         call(S, Set1),
179.         call(S, Set2),
180.         Set1 \= Set2,
181.         intersection(Set1, Set2, _)
182.     )).
183.
184.
185. domain(succ, fin(10)).
186. domain(restriction(R,S),intersection(D,S)) :- domain(R,D).
187. domain(reflexive_closure(R),S) :- domain(R,S).
188. domain(symmetric_closure(R),S) :- domain(R,S).
189. domain(transitive_closure(R),S) :- domain(R,S).
190. domain(l1, fin(12)).
191. domain(l2, fin(5)).
192. domain(l3, fin(3)).
193. domain(l4, fin(3)).
194. domain(l5, fin(15)).
195. domain(oh1, fin(3)).
196. domain(r, fin(4)).
197.
198. % the set of all prolog terms
199. any(_).
200.
201. % the empty-set.
202. % redundant rule, could simply be represented by the absence of any rule for `none`,
203. % but serves the purpose of preventing none from being defined differently elsewhere,
204. % and indicates the intention of this predicate.
205. none(_) :- false.
206.
207. restriction(R, S, X, Y) :-
208.     call(S, X),
209.     call(S, Y),
210.     call(R, X, Y).
211.
212. reverse(R, X, Y) :-
213.     call(R, Y, X).
214.
215. pred(X, Y) :-
216.     reverse(succ, X, Y).
217.
218. % reflexive closure of R is the minimal reflexive relation containing R
219. % * reflexivity is interpreted as being restricted to the domain
220. % * equivalent to union of R with loops(domain(R)), and indeed that's how it's implemented here
221. % * need to know the domain in order to generate reflexive closure
222. % issue: doesn't filter repeats
223. /*
224. reflexive_closure(R, X, Y) :-
225.     (
226.         call(R, X, Y) % contains(reflexive_closure(R),R)
227.     ;
228.         (
229.             domain(R,S),
230.             call(S,X),
231.             call(S,Y),
232.             X = Y
233.         )
234.     ).
235. */
236.
237. % this one filters repeats
238. reflexive_closure(R, X, Y) :- call(R, X, Y).
239. reflexive_closure(R, X, X) :- domain(R, S), call(S, X), \+call(R, X, X).
240.
241. % symmetric closure of R is the minimal symmetric relation containing R
242. % * equivalent to union of R with reverse(R), and indeed that's how it's implemented here
243. % * don't need to know the domain in order to generate the symmetric closure, can be generated purely from the components of the relation
244. % issue: doesn't filter repeats
245. /*
246. symmetric_closure(R, X, Y) :-
247.     (
248.         call(R, X, Y) % contains(symmetric_closure(R),R)
249.     ;
250.         call(R, Y, X)
251.     ).
252. */
253.
254. % this one filters repeats
255. symmetric_closure(R, X, Y) :- call(R,X,Y).
256. symmetric_closure(R, X, Y) :- call(R,Y,X), \+call(R, X, Y).
257.
258. % transitive closure of R is the minimal transitive relation containing R
259. /*
260. TC(R,R*) :=
261.     contains(R*,R),
262.     transitive(R*),
263.     forall R',
264.         contains(R',R),
265.         transitive(R'),
266.     ->  contains(R',R*).
267. */
268. % issue: doesn't filter repeats
269. % goes into infinite loops
270. % should filter repeats and shouldn't go into infinite loops at least on finite relations
271. % under what conditions does it go into infinite loops on finite relations?
272. transitive_closure(R, X, Y) :-
273.     (
274.         call(R, X, Y)   % contains(transitive_closure(R),R)
275.     ;
276.         (
277.             call(R, X, Z),
278.             transitive_closure(R, Z, Y)
279.         )
280.     ).
281.
282. % transitive closure ~ path-space
283. /*
284. path-space is a bit more complicated notion
285.
286. */
287.
288. /*
289. generic closure:
290. closure(P,R,R') :=
291.     contains(R',R),
292.     P(R'),
293.     forall R'',
294.         contains(R'',R),
295.         P(R''),
296.     ->  contains(R'',R').
297.
298.
299. minimal(R,A) :=
300.     A(R),
301.     forall R',
302.         A(R')
303.     ->  contains(R',R).
304.
305. closure(P,R,R') :=
306.     minimal(
307.         R',
308.         [R'']>>(
309.             contains(R'',R),
310.             P(R'')
311.         )
312.     ).
313.
314. closure(P,R,X,Y) :-
315.     (
316.         call(R, X, Y)
317.     ;
318.         call(P, R, X, Y)
319.     ).
320. % not quite because transitive closure needs to recurse
321.
322.
323.
324. */
325.
326. lt(X,Y) :-
327.     transitive_closure(succ,X,Y).
328.
329. lte(X,Y) :-
330.     reflexive_closure(transitive_closure(succ),X,Y).
331.
332. % gt
333. % gte
334.
335. connected(R, X, Y) :-
336.     reflexive_closure(symmetric_closure(transitive_closure(R)),X,Y).
337.
338. connected_component_of(R, X, Component) :-
339.     findall(Y, connected(R, X, Y), Component).
340.
341. connected_component_helper(_, [], Components, Components).
342. connected_component_helper(R, [X | Rest], Current_Components, Components) :-
343.     member(Component, Current_Components),
344.     member(X, Component),
345.     !,
346.     connected_component_helper(R, Rest, Current_Components, Components).
347. connected_component_helper(R, [X | Rest], Current_Components, Components) :-
348.     connected_component_of(R, X, Component),
349.     connected_component_helper(R, Rest, [Component | Current_Components], Components).
350.
351. % a connected component is a maximal connected subset
352. % domain(R,Domain),
353. % subset(Domain, Subset),
354. % connected
355. connected_component(R, Component) :-
356.     findall(X, (call(R,X,_) ; call(R,_,X)), S),
357.     connected_component_helper(R, S, [], Components),
358.     member(Component, Components).
359.
360. connected_components(R, Components) :-
361.     findall(Component, connected_component(R,Component), Components).
362.
363. % issue: only needs to check (n-1) pairs
364. /*
365. relation_connected(R) :-
366.     domain(R, A),
367.     forall(A, [X]>>(
368.         forall(A, [Y]>>(
369.             connected(R, X, Y)
370.         ))
371.     )).
372. */
373. relation_connected(R) :-
374.     domain(R, A),
375.     call(A,X),
376.     !,
377.     call(A,Y),
378.     connected(R,X,Y).
379.
380. % issue: more efficient way than looping over powerset?
381. maximal_subset(P, S, T) :-
382.     powerset(S,T),
383.     call(P, T),
384.     \+((
385.         call(S, X),
386.         \+call(T,X),
387.         call(P, union(T,set([X])))
388.     )).
389.
390. % maximal connected subsets
391. % all the non-maximal connected subsets are contained by maximal connected subsets
392. connected_component2(R, C) :-
393.     domain(R, A),
394.     maximal_subset([S]>>(relation_connected(restriction(R,S))), A, C).
395.
396. connected_components2(R,Components) :-
397.     findall(Component, connected_component2(R,Component), Components).
398.
399. is_function(F,A,B) :-
400.     forall(A, [X]>>(findall(Y, (call(F,X,Y), call(B,Y)), [_]))).
401.
402. function_helper([], _, []).
403. function_helper([X|As], B, [(X,Y)|Rest]) :-
404.     call(B, Y),
405.     function_helper(As,B,Rest).
406.
407. % there's |B|^|A| functions A -> B
408. % 0^0 = 1 function (identity function) from the empty set to itself
409. function(eval(F),A,B) :-
410.     findall(X, call(A,X), As),
411.     function_helper(As, B, F).
412.
413.
414. % assumes that F is a function, i.e. passes is_function check
415. % how many injections A -> B ?
416. % 0 when |A| > |B|
417. % when |A| <= |B|, there are |B|!/(|B|-|A|)! injections
418. % when |A| = |B| = n, there are n! injections
419. % (|B| choose |A|)*A! ?
420. is_injective(F,_,_) :-
421.     \+((
422.         call(F,X1,Y),
423.         call(F,X2,Y),
424.         X1 \= X2
425.     )).
426.
427. injection(F,A,B) :-
428.     function(F,A,B),
429.     is_injective(F,A,B).
430.
431. % assumes that F is a function
432. % how many surjections A -> B ?
433. % 0 when |A| < |B|
434. % when |A| >= |B|, ...
435. % when |A| >= |B| = n,  there are n! surjections
436. % restatement using forall?
437. is_surjective(F,_,B) :-
438.     \+((
439.         call(B,Y),
440.         \+call(F,_,Y)
441.     )).
442.
443. surjection(F,A,B) :-
444.     function(F,A,B),
445.     is_surjective(F,A,B).
446.
447. % assumes that F is a function
448. % 0 when |A| \= |B|
449. % when |A| = |B| = n, there are n! bijections
450. is_bijective(F,A,B) :-
451.     is_injective(F,A,B),
452.     is_surjective(F,A,B).
453.
454. bijection(F,A,B) :-
455.     function(F,A,B),
456.     is_bijective(F,A,B).
457.
458.
459. % assumes F is a function
460. % restatement using forall?
461. is_order_homomorphism(F,(A,A_Order),(_,B_Order)) :-
462.     \+((
463.         call(A, X1),
464.         call(A, X2),
465.         call(A_Order, X1, X2),
466.         call(F, X1, Y1),
467.         call(F, X2, Y2),
468.         \+ call(B_Order, Y1, Y2)
469.     )).
470.
471. order_homomorphism(F,(A, A_Order),(B, B_Order)) :-
472.     function(F,A,B),
473.     is_order_homomorphism(F, (A, A_Order), (B, B_Order)).
474.
475. occurrence((S1, S1_Order), (S2, S2_Order), F) :-
476.     domain(S1, S1_Domain),
477.     domain(S2, S2_Domain),
478.     order_homomorphism(F, (S1_Domain, S1_Order), (S2_Domain, S2_Order)),
479.     relation_equality(S1, compose(S2,F)).
480.
481. find(S1, S2, F) :-
482.     occurrence(S1, S2, F).
483.
484. image(F,Y) :-
485.     call(F,_,Y).
486.
487. something :-
488.     findall(
489.         Occurrence,
490.         occurrence((l3, restriction(succ,fin(3))), (l2, restriction(succ,fin(5))), Occurrence),
491.         Occurrences
492.     ),
493.     intersection_set([Y]>>(member(X,Occurrences), Y = image(X)), Both),
494.     writeln(Both).
495.
496.
497. eval(F,X,Y) :- member((X,Y),F).
498.
499. cardinality(S,N) :-
500.     findall(X,call(S,X),Reified),
501.     length(Reified, N).
502.
503. powerset(S,Subset) :-
504.     function(F,S,bool),
505.     Subset = [X]>>(call(F,X,t)).
506.
507.
508. bool(t).
509. bool(f).
510.
511. color(red).
512. color(blue).
513. color(green).
514.
515. color2(red).
516. color2(blue).
517. color2(yellow).
518.
519. compose(G, F, X, Z) :-
520.     call(F, X, Y),
521.     call(G, Y, Z).
522.
523. cyclic(R) :-
524.     domain(R,A),
525.     call(A,X),
526.     transitive_closure(R,X,X).
527.
528. /*
529. contains(R, Q) :-
530.     domain(R,A),
531.     domain(Q,A),
532.     forall(A, [X]>>(
533.         forall(A, [Y]>>(
534.             call(Q, X, Y) -> call(R, X, Y)
535.         )
536.     ).
537. */
538. % this version works with unspecified domain:
539. % this only works when Q is enumerable
540. contains(R, Q) :-
541.     \+((
542.         call(Q, X, Y),
543.         \+ call(R, X, Y)
544.     )).
545.
546. /*
547. minimal(R, P) :-
548.     call(P, R),
549.     forall(relation(2),
550.         [S]>>(
551.             call(P, S) -> contains(S,R)
552.         )
553.     ).
554.
555. closure(R, P, S) :-
556.     minimal(S, [X]>>(contains(X,R), call(P, X))).
557. */
558.
559. not(P, X) :-
560.     \+ call(P, X).
561.
562. %minimal(R,A) :-
563.
564. % exhaustive search for
565. % intersection of A and P?
566. % what about version that doesn't cut?
567. exists(A,P) :-
568.     call(A, X),
569.     call(P, X),
570.     !.
571.
572.
573. % this only works when A is enumerable
574. forall(A,P) :-
575.     \+ exists(A, not(P)).
576. % get cycles
577. /*
578. sublists defined by injective order homomorphisms into the domain of the list?
579. * connected subsets of the domain
580. */
581.
582. % permutations
583. % number of permutations of finite set S with |S| = n is n!
584. % number of functions S -> S is n^n
585. % is also the number of bijections S -> S
586.
587.
588. % permute a function by composing the function with a permutation of its domain
589.
590. /*
591. find every injective order homomorphism
592. * find every function and check if it's an order homomorphism
593. */
594.
595. /*
596. need order induced on connected components and to put them in this proper list order
597.
598.
599. */
600.
601. % select disjoint subsets of match-set:
602. /*
603. maximal_disjoint_subset(S, T) :-
604.     powerset(S, T),
605.     disjoint_set(T),
606.     \+((
607.         call(S, X),
608.         \+call(T, X),
609.         disjoint_set(union(T, set([X])))
610.     )).
611. */
612. set(L, X) :-
613.     member(X, L).
614.
615. /*
616. maximal_disjoint_subset(S, T) :-
617.     powerset(S, T),
618.     disjoint_set(T),
619.     forall(S, [X]>>(
620.         (
621.             call(T, X)
622.         ;
623.             \+disjoint_set(union(T, set([X])))
624.         )
625.     )).
626. */
627.
628. maximal_disjoint_subset(S, T) :-
629.     maximal_subset(disjoint_set, S, T).
630.
631. set_of(Template, Goal, [X]>>(member(X,List))) :-
632.     findall(Template, Goal, List).
633.
634. functions_disjoint(F, G) :-
635.     disjoint(image(F), image(G)).
636.
637.
638.
639. split(String, Delimiter, Components) :-
640.     % set of (images of) matches (subsets of String_Index)
641.     set_of(
642.         image(Match),
643.         find(Delimiter, String, Match),
644.         Image_Set
645.     ),
646.
647.     % maximal disjoint subset of matches
648.     maximal_disjoint_subset(Image_Set, Subset),
649.
650.     %
651.     String = (S, _),
652.     domain(S, String_Index),
653.     R = restriction(succ, difference(String_Index, union_set(Subset))),
654.
655.     % connected components of rest of string
656.     connected_components(R, Components).
657.
658.     % each component should be string-ordered
659.
660. split_if(String, Delimiter, Components) :-
661.     word(String, S),
662.     word(Delimiter, D),
663.     split(S, D, Components).
664.
665. word(S, (S, restriction(succ, Domain))) :- domain(S, Domain).
666.
667.
668.
669. relation_equality(R1, R2) :-
670.     contains(R1, R2),
671.     contains(R2, R1).
672.
673. % ex..
674. /*
675.
676. ?- relation_equality(l3, compose(l2,oh1)).
677. true.
678.
679. */
680.
681. % function equality is just relation equality when both relations are functions
682. % if necessary, add an is_function check.
683.
684.
685. /*
686. find(Search, List, Matches) :-
687.     findall(
688.         Match,
689.         (
690.             call(List, Index, Item),
691.
692.         ),
693.         Matches
694.     ).
695. */
696. /*
697. connected_components(R, Components) :-
698. */
699. % dealing with the infinite
700. % dealing with complexity
702. % dealing with arbitrary arities of relations
703. % dealing with domains and codomains
704.
705. % BDDs
706. % counterexample-guided abstraction refinement (CEGAR)
707.
708. /*
709. isomorphism between lists and finite totally-ordered sets
710.
711. */
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top