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
  701. %  * start with brute-force, weed out search paths?
  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. OK, I Understand
 
Top