-
Notifications
You must be signed in to change notification settings - Fork 0
/
metadl.dl
190 lines (157 loc) · 10 KB
/
metadl.dl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
// TODO support symbol values?
.type Argument = Constant { value: number }
| Variable { name: symbol }
.type ConstantList = [
first: number,
rest: ConstantList
]
.type ArgumentList = [
first: Argument,
rest: ArgumentList
]
.type Predicate = [
name: symbol,
arguments: ArgumentList
]
.type PredicateList = [
first: Predicate,
rest: PredicateList
]
.type HornClause = [
head: Predicate,
body: PredicateList
]
.type VariableList = [
first: symbol,
rest: VariableList
]
.type Substitution = [
variable_name: symbol,
value: number
]
.type SubstitutionList = [
first: Substitution,
rest: SubstitutionList
]
.decl extensional(rule: HornClause)
// parent(0, 1).
extensional([["parent", [$Constant(0), [$Constant(1), nil]]],
nil]).
// parent(1, 2).
extensional([["parent", [$Constant(1), [$Constant(2), nil]]],
nil]).
// parent(1, -2).
extensional([["parent", [$Constant(1), [$Constant(-2), nil]]],
nil]).
// parent(2, 3).
extensional([["parent", [$Constant(2), [$Constant(3), nil]]],
nil]).
// ancestor(x, y) :- parent(x, y).
extensional([["ancestor", [$Variable("x"), [$Variable("y"), nil]]],
[["parent", [$Variable("x"), [$Variable("y"), nil]]], nil]]).
// ancestor(x, y) :- ancestor(x, z), parent(z, y).
extensional([["ancestor", [$Variable("x"), [$Variable("y"), nil]]],
[["ancestor", [$Variable("x"), [$Variable("z"), nil]]], [["parent", [$Variable("z"), [$Variable("y"), nil]]], nil]]]).
// same_parent(x, y) :- parent(p, x), parent(p, y).
extensional([["same_parent", [$Variable("x"), [$Variable("y"), nil]]],
[["parent", [$Variable("p"), [$Variable("x"), nil]]], [["parent", [$Variable("p"), [$Variable("y"), nil]]], nil]]]).
.decl body_predicate(rule: HornClause, predicate: Predicate, rest_preds: PredicateList)
body_predicate(rule, p, restpreds) :- extensional(rule), rule=[_1, [p, restpreds]].
body_predicate(rule, p, restpreds) :- body_predicate(rule, _, [p, restpreds]).
.decl body_argument(rule: HornClause, argument: Argument, rest_args: ArgumentList)
body_argument(rule, arg, restargs) :- body_predicate(rule, [_, [arg, restargs]], _).
body_argument(rule, arg, restargs) :- body_argument(rule, _, [arg, restargs]).
.decl head_argument(rule: HornClause, argument: Argument, rest_args: ArgumentList)
head_argument(rule, arg, restargs) :-
extensional(rule),
rule=[[_1, [arg, restargs]], _2].
head_argument(rule, arg, restargs) :- head_argument(rule, _, [arg, restargs]).
// Report rules that contain a variable in the head that is not an
// argument of any predicate in the body.
.decl error_ungrounded_variable(ungrounded_variable: Argument, rule: HornClause)
.output error_ungrounded_variable(IO=stdout, delimiter=" is ungrounded in ")
error_ungrounded_variable(ungrounded_var, rule) :-
head_argument(rule, ungrounded_var, _),
ungrounded_var=$Variable(_1),
!body_argument(rule, ungrounded_var, _).
// The set of extensional facts (but constants is in reverse order)
// No groundedness check necessary because extensional_fact_rev_(_, _, nil) will only exist when all arguments are constants.
.decl extensional_fact_rev_(predicate_name: symbol, constants: ConstantList, args_rest: ArgumentList)
extensional_fact_rev_(pname, nil, args) :- extensional([[pname, args], nil]).
extensional_fact_rev_(pname, [c, restcs], restargs) :- extensional_fact_rev_(pname, restcs, [$Constant(c), restargs]).
.decl extensional_fact_(predicate_name: symbol, constants: ConstantList, rev_constants: ConstantList)
extensional_fact_(pname, nil, revcs) :- extensional_fact_rev_(pname, revcs, nil).
extensional_fact_(pname, [c, restcs], revcs) :- extensional_fact_(pname, restcs, [c, revcs]).
.decl extensional_fact(predicate_name: symbol, constants: ConstantList)
extensional_fact(pname, cs) :- extensional_fact_(pname, cs, nil).
// The set of variables that appear in the body of a rule. Duplicates may be present.
.decl rule_variables_(rule: HornClause, variable_names: VariableList, rest_args: ArgumentList, rest_preds: PredicateList)
rule_variables_(rule, nil, args, restpreds) :- extensional(rule), rule = [_1, [[_2, args], restpreds]].
rule_variables_(rule, vnames, args, restpreds) :- rule_variables_(rule, vnames, nil, [[_, args], restpreds]).
rule_variables_(rule, vnames, restargs, restpreds) :- rule_variables_(rule, vnames, [$Constant(_), restargs], restpreds).
rule_variables_(rule, [vname, vnames], restargs, restpreds) :- rule_variables_(rule, vnames, [$Variable(vname), restargs], restpreds).
.decl rule_variables(rule: HornClause, variable_names: VariableList)
rule_variables(rule, vnames) :- rule_variables_(rule, vnames, nil, nil).
// The deduplicated version of rule_variables. It's also in reverse
// order but that is irrelevant for substitutions.
// This is modeled after samples/deduplicate.dl.
.decl rule_variables_dedup_(rule: HornClause, result: VariableList, tocheck: VariableList, todo: VariableList)
rule_variables_dedup_(rule, nil, nil, x) :- rule_variables(rule, x).
// When the top of tocheck has been seen before, leave output unchanged and consider the rest of tocheck.
rule_variables_dedup_(rule, r, nil, trest) :- rule_variables_dedup_(rule, r, [s, _], [s, trest]).
// When the top of todo was nowhere in result, move it to result.
rule_variables_dedup_(rule, [e, result], [e, result], trest) :- rule_variables_dedup_(rule, result, nil, [e, trest]).
// Keep looking when we haven't proved or disproved that the top of todo is in result.
rule_variables_dedup_(rule, r, tocheckrest, [e, trest]) :- rule_variables_dedup_(rule, r, [tocheck, tocheckrest], [e, trest]), tocheck != e.
.decl rule_variables_dedup(rule: HornClause, result: VariableList)
rule_variables_dedup(rule, vnames) :- rule_variables_dedup_(rule, vnames, _, nil).
// The set of all constants in the program's facts.
.decl fact_constant_(constant: number, rest: ConstantList)
fact_constant_(c, crest) :- fact_rev(_, [c, crest]).
fact_constant_(c, crest) :- fact_constant_(_, [c, crest]).
// The set of substitutions that can be applied for a particular rule.
// This is the starting point for bottom-up evaluation: generate all substitutions so later we can exhaustively try them.
.decl possible_substitution_(rule: HornClause, subs: SubstitutionList, variables_rest: VariableList)
possible_substitution_(rule, nil, vars) :- rule_variables_dedup(rule, vars).
possible_substitution_(rule, [[vname, c], srest], vrest) :- possible_substitution_(rule, srest, [vname, vrest]), fact_constant_(c, _).
.decl possible_substitution(rule: HornClause, subs: SubstitutionList)
possible_substitution(rule, subs) :- possible_substitution_(rule, subs, nil).
// Now apply the possible substitutions on the rules.
.decl substitution_lookup(subs: SubstitutionList, variable_name: symbol, value: number, rest: SubstitutionList)
substitution_lookup(subs, var, v, rest) :- possible_substitution(_, subs), subs=[[var, v], rest].
substitution_lookup(subs, var, v, rest) :- substitution_lookup(subs, _1, _2, [[var, v], rest]).
.decl substitution_(rule: HornClause, subs: SubstitutionList, curr_pred_name: symbol, constants: ConstantList, arg_rest: ArgumentList, prest: PredicateList)
// Note it's OK to work only on rules with >= 1 predicates because otherwise it's just an extensional fact.
substitution_(rule, subs, pname, nil, args, prest) :- possible_substitution(rule, subs), rule=[_1, [[pname, args], prest]].
// Constants are unchanged by substitution.
substitution_(rule, subs, pname, [c, crest], arest, prest) :- substitution_(rule, subs, pname, crest, [$Constant(c), arest], prest).
// Variables are transformed according to subs.
substitution_(rule, subs, pname, [c, crest], arest, prest) :- substitution_(rule, subs, pname, crest, [$Variable(vname), arest], prest), substitution_lookup(subs, vname, c, _).
// When finished with substitution of a predicate, we check that it is satisfied by an existing rule.
// If so, we either move on to checking the rest of the body or, if we checked the entire body, we are done and the substitution has 'succeeded'.
// (note we check against fact_rev because cs has been built up in reverse order)
substitution_(rule, subs, next_pname, nil, next_args, prest) :- substitution_(rule, subs, pname, cs, nil, [[next_pname, next_args], prest]), fact_rev(pname, cs).
.decl successful_substitution(rule: HornClause, subs: SubstitutionList)
successful_substitution(rule, subs) :- substitution_(rule, subs, pname, cs, nil, nil), fact_rev(pname, cs).
// Now apply substitution to the head of rules in successful_substitution, which will represent an intensional fact.
.decl head_substitution_rev_(head_name: symbol, substituted_args: ConstantList, subs: SubstitutionList, arg_rest: ArgumentList)
head_substitution_rev_(hname, nil, subs, args) :- successful_substitution([[hname, args], _], subs).
head_substitution_rev_(hname, [c, cs], subs, arest) :- head_substitution_rev_(hname, cs, subs, [$Constant(c), arest]).
head_substitution_rev_(hname, [c, cs], subs, arest) :- head_substitution_rev_(hname, cs, subs, [$Variable(vname), arest]), substitution_lookup(subs, vname, c, _).
// And lastly reverse so that things are in order.
.decl head_substitution_(head_name: symbol, result: ConstantList, input_rest: ConstantList)
head_substitution_(hname, nil, cs) :- head_substitution_rev_(hname, cs, _, nil).
head_substitution_(hname, [c, crest], inrest) :- head_substitution_(hname, crest, [c, inrest]).
.decl intensional_fact(head_name: symbol, constants: ConstantList)
intensional_fact(hname, cs) :- head_substitution_(hname, cs, nil).
// The set of all facts in the metadatalog program, extensional and intensional.
// Also available with constants in reverse order, which is convenient for the
// substitution-checking phase.
.decl fact(predicate_name: symbol, constants: ConstantList)
fact(pname, cs) :- extensional_fact(pname, cs).
fact(pname, cs) :- intensional_fact(pname, cs).
.decl fact_rev(predicate_name: symbol, constants: ConstantList)
fact_rev(pname, cs) :- extensional_fact_rev_(pname, cs, nil).
fact_rev(pname, cs) :- head_substitution_rev_(pname, cs, _, nil).
.output extensional_fact(IO=stdout)
.output intensional_fact(IO=stdout)