Skip to content

Commit bb59bd6

Browse files
albschalbsch
committed
[recsys] Inductive predicate for recursive systems
1 parent fb98d99 commit bb59bd6

File tree

7 files changed

+384
-0
lines changed

7 files changed

+384
-0
lines changed

‎README.md‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
```mermaid
2+
graph TD;
3+
dnf[Representations of DNF]-->bdd;
4+
dnf-->dnfsimpl[Simplifications on DNF];
5+
dnf-->lol[List of Lists];
6+
lol-->musem;
7+
musem-->semsimpl[Semantic Type Simplification];
8+
bdd[Binary Decision Diagrams]-->bddsem;
9+
recsys[Recursive Systems<br>recsys]-->musem[Minimal Subtype Predicate<br>musem];
10+
recsys-->recbasic[Basic System];
11+
recsys-->reccache[Caching Recursive System];
12+
recsys-->recbacktrack[Backtrack-free Recursive System];
13+
recsys-->parse[Parsing Recursive Types];
14+
musem-->muhash[Equivalence Classes and Hashing<br>muhash];
15+
musem-->bddsem[Binary Decision Diagrams for Semantic Subtyping<br>bddsem];
16+
bddsem-->erlsem[Subtyping with Erlang Types<br>erlsem];
17+
erlsem-->etylizer[Etylizer];
18+
recbasic-->etylizer;
19+
parse-->etylizer;
20+
```

‎apps/recsys/src/inductive.erl‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
-module(inductive).
2+
3+
-compile([export_all, nowarn_unused_type, nowarn_export_all]).
4+
5+
% This module implements 7.1 of Frischs PhD thesis to study caching behavior of recursive systems.
6+
%
7+
% p =
8+
% t
9+
% | 0
10+
% | 1
11+
% | p U p
12+
% | p & p
13+
-type phi() ::
14+
variable()
15+
| 0
16+
| 1
17+
| {'or', phi(), phi()}
18+
| {'and', phi(), phi()}.
19+
-type system() :: #{variable() => phi()}.
20+
21+
-type variable() :: atom().

‎apps/recsys/src/inductive_basic.erl‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
-module(inductive_basic).
2+
3+
-compile([export_all, nowarn_unused_type, nowarn_export_all]).
4+
5+
-type phi() :: inductive:phi().
6+
-type variable() :: inductive:variable().
7+
-type system() :: inductive:system().
8+
-type result() :: 0 | 1.
9+
-type 'N'() :: #{variable() => 0}.
10+
11+
-spec
12+
sat(phi(), system(), 'N'()) -> result().
13+
sat(1, _S, _N) -> 1;
14+
sat(0, _S, _N) -> 0;
15+
sat({'or', Phi1, Phi2}, S, N) ->
16+
case sat(Phi1, S, N) of
17+
1 -> 1;
18+
0 -> sat(Phi2, S, N)
19+
end;
20+
sat({'and', Phi1, Phi2}, S, N) ->
21+
case sat(Phi1, S, N) of
22+
0 -> 0;
23+
1 -> sat(Phi2, S, N)
24+
end;
25+
sat(Variable, S, N) ->
26+
case S of #{Variable := Phi} ->
27+
case N of
28+
#{Variable := 0} -> 0;
29+
_ ->
30+
sat(Phi, S, N#{Variable => 0})
31+
end
32+
;_->error(bad_system)end.
33+
34+
-spec 'Example 7.16_test'() -> ok.
35+
'Example 7.16_test'() ->
36+
S = #{
37+
t1 => {'or', t2, 1},
38+
t2 => t1
39+
},
40+
1 = sat(t1, S, #{}).
41+
42+
-spec 'Example 7.17_test'() -> ok.
43+
'Example 7.17_test'() ->
44+
S = #{
45+
t1 => {'or', t2, 1},
46+
t2 => 0
47+
},
48+
1 = sat(t1, S, #{}).
49+
50+
-spec 'Example 7.25_test'() -> ok.
51+
'Example 7.25_test'() ->
52+
S = #{
53+
t1 => t2,
54+
t2 => t1
55+
},
56+
0 = sat(t1, S, #{}),
57+
ok.

‎apps/recsys/src/inductive_cache.erl‎

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
-module(inductive_cache).
2+
3+
-compile([export_all, nowarn_unused_type, nowarn_export_all]).
4+
5+
-type phi() :: inductive:phi().
6+
-type variable() :: inductive:variable().
7+
-type system() :: inductive:system().
8+
% result contains a positive and negative cache now
9+
% negative cache is only an approximation
10+
-type result() :: {0 | 1, 'N'(), 'P'()}.
11+
-type 'N'() :: #{variable() => 0}.
12+
-type 'P'() :: #{variable() => 1}.
13+
14+
-spec eval(phi(), system(), 'N'(), 'P'()) -> result().
15+
eval(0, _S, N, P) -> {0, N, P};
16+
eval(1, _S, N, P) -> {1, N, P};
17+
eval({'or', Phi1, Phi2}, S, N, P) ->
18+
case eval(Phi1, S, N, P) of
19+
{1, Np, Pp} -> {1, Np, Pp};
20+
{0, Np, Pp} -> eval(Phi2, S, Np, Pp)
21+
end;
22+
eval({'and', Phi1, Phi2}, S, N, P) ->
23+
case eval(Phi1, S, N, P) of
24+
{0, Np, Pp} -> {0, Np, Pp};
25+
{1, Np, Pp} -> eval(Phi2, S, Np, Pp)
26+
end;
27+
eval(Variable, S, N, P) ->
28+
case S of #{Variable := Phi} ->
29+
case P of
30+
#{Variable := 1} -> {1, N, P};
31+
_ ->
32+
case N of
33+
#{Variable := 0} -> {0, N, P};
34+
_ ->
35+
case eval(Phi, S, N#{Variable => 0}, P) of
36+
{0, Nn, Pp} -> {0, Nn, Pp};
37+
{1, _Nn, Pp} -> {1, N, Pp#{Variable => 1}} % invalidate formulas added to N (possibly many)
38+
end
39+
end
40+
end
41+
end.
42+
43+
-spec 'Example 7.16_test'() -> ok.
44+
'Example 7.16_test'() ->
45+
S = #{
46+
t1 => {'or', t2, 1},
47+
t2 => t1
48+
},
49+
{1, #{}, #{t1 := 1}} = eval(t1, S, #{}, #{}),
50+
ok.
51+
52+
-spec 'Example 7.17_test'() -> ok.
53+
'Example 7.17_test'() ->
54+
S = #{
55+
t1 => {'or', t2, 1},
56+
t2 => 0
57+
},
58+
% cache misses that t2 is 0 and does not depend on t1 during computation, false dependency is added
59+
% we would like t2 := 0 to be in the N result cache
60+
{1, #{}, #{t1 := 1}} = eval(t1, S, #{}, #{}),
61+
ok.
62+
63+
-spec 'Example 7.25_test'() -> ok.
64+
'Example 7.25_test'() ->
65+
S = #{
66+
t1 => t2,
67+
t2 => t1
68+
},
69+
% both t1 and t2 are empty, but we can't cache it
70+
{0, #{}, #{}} = eval(t1, S, #{}, #{}),
71+
ok.
72+
73+
cache_test() ->
74+
S = #{
75+
t1 => {'and', t2, {'and', t2, 1}},
76+
t2 => 1
77+
},
78+
% cache computes t2 only once
79+
{1, #{}, #{t1 := 1, t2 := 1}} = eval(t1, S, #{}, #{}).

‎apps/recsys/src/inductive_no_backtrack.erl‎

Lines changed: 137 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,137 @@
1+
-module(inductive_no_backtrack).
2+
3+
-compile([export_all, nowarn_unused_type, nowarn_export_all]).
4+
5+
-type phi() :: inductive:phi().
6+
-type variable() :: inductive:variable().
7+
8+
-type long_constraint() :: variable() | {phi(), long_constraint()}.
9+
-type table() :: #{variable() => 0 | 1 | [C_i :: long_constraint()]}. % with table(v(C_i)) not in {0, bottom}
10+
11+
-spec v(long_constraint()) -> variable().
12+
v({_, C}) -> v(C);
13+
v(Var) -> Var.
14+
15+
-spec domain(table()) -> sets:set(variable()).
16+
domain(O) ->
17+
% maps:keys(O).
18+
sets:from_list(maps:keys(O)).
19+
20+
-spec true_variables(table()) -> sets:set(variable()).
21+
true_variables(O) ->
22+
sets:from_list([Var || Var := 1 <- O]).
23+
24+
-spec leq(table(), table()) -> boolean().
25+
leq(O1, O2) ->
26+
sets:is_subset(domain(O2), domain(O1))
27+
and
28+
sets:is_subset(true_variables(O2), true_variables(O1)).
29+
30+
-spec extend(table(), variable(), todo) -> todo.
31+
extend(O, T, S) ->
32+
case O of
33+
#{T := _} -> O; % o(t) not bottom
34+
_ ->
35+
O0 = trigger(O#{T => []}, {maps:get(T, S), T}, S),
36+
% if the state of t is a set of constraints [C1; . . . ; Cn],
37+
% we can sometimes replaces it with 0, which will save us from extending this set later.
38+
% we have to be sure that t is indeed 0 first
39+
% that is the case if none of the other suspended constraints in the current table
40+
% is "pointing" towards t
41+
case may(O0, T, S) of
42+
true -> O0;
43+
false -> O0#{T => 0}
44+
end
45+
end.
46+
47+
trigger(O, C, S) ->
48+
Vc = v(C),
49+
case O of
50+
% when activating the constraint C,
51+
% if we know that the truth value of Vc is 1,
52+
% we can ignore this constraint
53+
#{Vc := 1} -> O;
54+
_ -> trigger2(O, C, S)
55+
end.
56+
57+
trigger2(O, T, S) when is_atom(T) ->
58+
#{T := L} = O,
59+
trigger3(O#{T => 1}, L, S);
60+
trigger2(O, {T, C}, S) when is_atom(T) ->
61+
case v(C) of
62+
% a constraint of the form t => ... => t can be ignored
63+
T -> O;
64+
_ ->
65+
O0 = extend(O, T, S),
66+
case O0 of
67+
#{T := 0} -> O0;
68+
#{T := 1} -> trigger(O0, C, S);
69+
#{T := L} ->
70+
O0#{T => [C | L]}
71+
end
72+
end;
73+
trigger2(O, {0, _C}, _S) -> O;
74+
trigger2(O, {1, C}, S) -> trigger2(O, C, S);
75+
trigger2(O, {{'and', F1, F2}, C}, S) -> trigger2(O, {F1, {F2, C}}, S);
76+
trigger2(O, {{'or', F1, F2}, C}, S) -> trigger(trigger2(O, {F1, C}, S), {F2, C}, S).
77+
78+
trigger3(O, [], _S) -> O;
79+
trigger3(O, [C | L], S) -> trigger3(trigger(O, C, S), L, S).
80+
81+
82+
% assumption: T is in O
83+
may(O, T, _S) ->
84+
case O of
85+
#{T := 1} -> true;
86+
_ ->
87+
length([ok || _Tp := V <- O, is_list(V), lists:any(fun(C) -> case v(C) of T -> true; _ -> false end end, V) ]) > 0
88+
end.
89+
90+
clean(O) -> #{K => case V of 0 -> 0; 1 -> 1; _ -> 0 end || K := V <- O}.
91+
92+
93+
-spec 'Example 7.16_test'() -> ok.
94+
'Example 7.16_test'() ->
95+
S = #{
96+
t1 => {'or', t2, 1},
97+
t2 => t1
98+
},
99+
#{t1 := 1, t2 := 1} = extend(#{}, t1, S),
100+
ok.
101+
102+
-spec 'Example 7.17_test'() -> ok.
103+
'Example 7.17_test'() ->
104+
S = #{
105+
t1 => {'or', t2, 1},
106+
t2 => 0
107+
},
108+
% t2 := 0 is now in the negative cache
109+
#{t1 := 1, t2 := 0} = extend(#{}, t1, S),
110+
ok.
111+
112+
-spec 'Example 7.25_test'() -> ok.
113+
'Example 7.25_test'() ->
114+
S = #{
115+
t1 => t2,
116+
t2 => t1
117+
},
118+
#{t1 := 0, t2 := 0} = clean(extend(#{}, t1, S)),
119+
ok.
120+
121+
cache_test() ->
122+
S = #{
123+
t1 => {'and', t2, {'and', t2, 1}},
124+
t2 => 1
125+
},
126+
% cache computes t2 only once
127+
#{t1 := 1, t2 := 1} = extend(#{}, t1, S).
128+
129+
-spec shortcut_test() -> ok.
130+
shortcut_test() ->
131+
S = #{
132+
t1 => {'or', 1, t2},
133+
t2 => t1
134+
},
135+
% t2 is not explored
136+
#{t1 := 1} = extend(#{}, t1, S),
137+
ok.

‎apps/recsys/src/recsys.app.src‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
{application, recsys,
2+
[{description, "Inductive unary predicate for recursive formulae"},
3+
{vsn, "1.0.0"},
4+
{applications,
5+
[kernel,
6+
stdlib
7+
]}
8+
]}.

‎apps/recsys/test/prop_equiv.erl‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
-module(prop_equiv).
2+
3+
-include_lib("proper/include/proper.hrl").
4+
-include_lib("eunit/include/eunit.hrl").
5+
6+
-export([limited_formula/0]).
7+
8+
vars() -> [t1, t2, t3, t4, t5, t6, t7, t8, t9, t10].
9+
10+
limited_formula() ->
11+
?SIZED(Size, limited_formula(Size)).
12+
13+
limited_formula(Size) when Size =< 1 ->
14+
frequency([
15+
{1, 0},
16+
{1, 1},
17+
{1, oneof(vars())}
18+
]);
19+
limited_formula(Size) ->
20+
frequency([
21+
{1, 0},
22+
{1, 1},
23+
{1, oneof(vars())},
24+
{2, ?LAZY(?LET({A, B},
25+
{limited_formula(Size - 1), limited_formula(Size - 1)},
26+
{'and', A, B})) },
27+
{2, ?LAZY(?LET({A, B},
28+
{limited_formula(Size - 1), limited_formula(Size - 1)},
29+
{'or', A, B})) }
30+
]).
31+
32+
system(Variables) ->
33+
?LET(Formulas, [limited_formula() || _ <- Variables],
34+
maps:from_list(lists:zip(Variables, Formulas))
35+
).
36+
37+
% prop_print() ->
38+
% ?FORALL( X, system(), begin io:format(user, "~p~n", [X]), true end).
39+
40+
prop_equiv() ->
41+
Vars = vars(),
42+
?FORALL(X, system(Vars),
43+
begin
44+
lists:all(fun(Var) ->
45+
46+
{T, Result} = timer:tc(fun() -> inductive_basic:sat(Var, X, #{}) end),
47+
{T2, {Result, _, _}} = timer:tc(fun() -> inductive_cache:eval(Var, X, #{}, #{}) end),
48+
{T3, #{Var := Result}} = timer:tc(fun() -> inductive_no_backtrack:clean(inductive_no_backtrack:extend(#{}, Var, X)) end),
49+
50+
case {T, T2, T3} of
51+
{0,0,0} -> ok;
52+
{Z, _, Z} when X > 2000 -> io:format(user,"Slow!~n~p~n", [{Var, X}]);
53+
_ ->
54+
io:format(user,"~p vs ~p vs ~p~n", [T, T2, T3])
55+
end,
56+
57+
58+
true
59+
% % v2
60+
% inductive_basic:sat(Var, X, #{}) =:= inductive_basic:sat_neg(Var, X, #{})
61+
end, Vars)
62+
end).

0 commit comments

Comments
 (0)