Skip to content

Commit 889fb46

Browse files
alex-quin-gabrielalex-quin-gabriel
authored
adding decision logic (#13)
* original inclusion of Tyler's decision system logic * adding tyler's decision logic including basic tests
1 parent a38d5d2 commit 889fb46

File tree

12 files changed

+1585
-12
lines changed

12 files changed

+1585
-12
lines changed

‎tff/domains/decision-system/engines.tff‎

Lines changed: 991 additions & 0 deletions
Large diffs are not rendered by default.

‎tff/domains/decision-system/properties.tff‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
% Originally contributed by Tyler Olson https://github.com/Rockjack00
2+
3+
% Decision properties for fixed parameters
4+
%include('/understanding-logic/tff/model/properties.tff').
5+
6+
%%%%%% Datatypes
7+
%---------------------------------------------------------------------------
8+
%%% Choice Size
9+
% TODO: This is not a datatype, it is a phenomenon. but right now there's not a way to express that...
10+
%-----------------------------------
11+
tff(choice_size_datatype_decl, type,
12+
choice_size_datatype : proptype
13+
).
14+
%-----------------------------------
15+
16+
%---------------------------------------------------------------------------
17+
18+
19+
20+
%%%%%% Properties
21+
%---------------------------------------------------------------------------
22+
%%% Decision Properties
23+
%-----------------------------------
24+
tff(absolute_size_prop_decl, type,
25+
absolute_size_prop : property
26+
).
27+
28+
tff(absolute_size_prop_datatype, axiom,
29+
type_of_property(absolute_size_prop) = choice_size_datatype
30+
).
31+
32+
%%% Choice properties
33+
%-----------------------------------
34+
tff(absolute_size_prop_decl, type,
35+
absolute_size_prop : property
36+
).
37+
38+
tff(n_parameter_prop_decl, type,
39+
n_parameter_prop : property
40+
).
41+
42+
tff(relation_parameter_prop_decl, type,
43+
relation_parameter_prop : property
44+
).
45+
46+
%-----------------------------------
47+
48+
tff(properties_are_distinct, axiom,
49+
$distinct(absolute_size_prop,
50+
n_parameter_prop,
51+
relation_parameter_prop
52+
)
53+
).

‎tff/model/engines.tff‎

Lines changed: 30 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,11 @@ tff(decl_engine_output_properties, type,
2626
tff(decl_engine_imparts_output_properties, type,
2727
engine_imparts_output_property: (engine * property) > $o
2828
).
29+
30+
% Engine outputs may retain properties
31+
tff(engine_transits_property_decl, type,
32+
engine_transits_property : (engine * property) > $o
33+
).
2934
%---
3035

3136
tff(decl_engine_output_formalism, type,
@@ -79,13 +84,13 @@ tff(formally_equivalent, axiom,
7984
modelet_models_concept(M, C)
8085
)
8186
&
82-
% ![R: representation_class]:
83-
% ( % Equivalence of processing model classes
84-
% template_has_representation_class_requirement(T, R)
85-
% =>
86-
% modelet_has_representation_class(M, R)
87-
% )
88-
% &
87+
![R: representation_class]:
88+
( % Equivalence of processing model classes
89+
template_has_representation_class_requirement(T, R)
90+
=>
91+
modelet_has_representation_class(M, R)
92+
)
93+
&
8994
! [SPT : spacetime_point]:
9095
(
9196
template_has_location_requirement(T, SPT)
@@ -137,3 +142,21 @@ tff(axiom_modelet_matches_template, axiom,
137142
inputs_match(M, T)
138143
)
139144
).
145+
146+
% Engines can conform to requirements
147+
tff(decl_engine_meets_requirement, type,
148+
engine_meets_requirement: (engine * requirement) > $o
149+
).
150+
151+
tff(axiom_engine_meets_requirement, axiom,
152+
! [E : engine, R : requirement, P: property]:
153+
(
154+
(
155+
engine_has_property(E, P) % match engine to property
156+
&
157+
property_meets_requirement(P, R)
158+
)
159+
=>
160+
engine_meets_requirement(E, R)
161+
)
162+
).

‎tff/model/one.tff‎

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,14 @@ tff(decl_exertable1, type,
2020
).
2121
% Modelets are exertable by Engines (no sets) 1
2222
tff(axiom_modelet_is_exertable1, axiom,
23-
![M: modelet, T: template, E: engine]:
23+
![M: modelet, T: template, E: engine, R: requirement]:
2424
(
2525
(
2626
inputs_match(M, T)
2727
&
2828
defines_input1(T, E)
29+
&
30+
(is_active(R) => engine_meets_requirement(E, R))
2931
)
3032
=>
3133
exertable1(E, M)
@@ -132,3 +134,21 @@ tff(axiom_engine_may_impart_property1, axiom,
132134
).
133135

134136

137+
138+
tff(axiom_engine_may_transit_property1, axiom,
139+
! [E: engine, IM1: modelet, OM: modelet, P: property]:
140+
(
141+
(
142+
exertable1(E, IM1)
143+
&
144+
exert1(E, IM1) = OM
145+
&
146+
engine_transits_property(E, P)
147+
&
148+
modelet_has_property(IM1, P)
149+
)
150+
=>
151+
modelet_has_property(OM, P)
152+
)
153+
).
154+

‎tff/model/properties-and-requirements.tff‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,9 @@ tff(decl_type_of_r, type,
2525
tff(decl_requirement_range, type,
2626
is_permissible: (requirement * $real) > $o).
2727

28+
% Requirements can be active, when applied to engines
29+
tff(decl_requirement_active, type,
30+
is_active: (requirement) > $o).
2831

2932
tff(property_meets_requirement_decl, type,
3033
property_meets_requirement : (property * requirement) > $o

‎tff/model/sets.tff‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -222,6 +222,30 @@ tff(axiom_engine_may_impart_property, axiom,
222222
)
223223
).
224224

225+
%%%%%% Transitive properties
226+
%---------------------------------------------------------------------------
227+
% An engine transits a property from any of its inputs to its output.
228+
% That is if any of its inputs have some property P, then its output will also
229+
% have that property P.
230+
tff(axiom_engine_transits_property, axiom,
231+
![E : engine, P : property, MS : modelet_set]:
232+
(
233+
(
234+
exertable(E, MS)
235+
&
236+
engine_transits_property(E, P)
237+
&
238+
?[Mparent : modelet]:
239+
(
240+
is_in_modelet_set(Mparent, MS)
241+
&
242+
modelet_has_property(Mparent, P)
243+
)
244+
)
245+
=>
246+
modelet_has_property(exert(E, MS), P)
247+
)
248+
).
225249

226250
%Engines produce reliable output
227251
%tff(axiom_engine_reliability, axiom,

‎tff/model/three.tff‎

Lines changed: 28 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ tff(decl_exertable3, type,
1919
).
2020
% Modelets are exertable by Engines (no sets) 3
2121
tff(axiom_modelet_is_exertable3, axiom,
22-
![M1: modelet, M2: modelet, M3: modelet, T1: template, T2: template, T3: template, E: engine]:
22+
![M1: modelet, M2: modelet, M3: modelet, T1: template, T2: template, T3: template, E: engine, R: requirement]:
2323
(
2424
(
2525
inputs_match(M1, T1)
@@ -29,6 +29,8 @@ tff(axiom_modelet_is_exertable3, axiom,
2929
inputs_match(M3, T3)
3030
&
3131
defines_input3(T1, T2, T3, E)
32+
&
33+
(is_active(R) => engine_meets_requirement(E, R))
3234
)
3335
=>
3436
exertable3(E, M1, M2, M3)
@@ -133,3 +135,28 @@ tff(axiom_engine_may_impart_property3, axiom,
133135
modelet_has_property(OM, P)
134136
)
135137
).
138+
139+
140+
141+
tff(axiom_engine_may_transit_property3, axiom,
142+
! [E: engine, IM1: modelet, IM2: modelet, IM3: modelet, OM: modelet, P: property]:
143+
(
144+
(
145+
exertable3(E, IM1, IM2, IM3)
146+
&
147+
exert3(E, IM1, IM2, IM3) = OM
148+
&
149+
engine_transits_property(E, P)
150+
&
151+
(
152+
modelet_has_property(IM1, P)
153+
|
154+
modelet_has_property(IM2, P)
155+
|
156+
modelet_has_property(IM3, P)
157+
)
158+
)
159+
=>
160+
modelet_has_property(OM, P)
161+
)
162+
).

‎tff/model/two.tff‎

Lines changed: 24 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,14 +20,16 @@ tff(decl_exertable2, type,
2020
).
2121
% Modelets are exertable by Engines (no sets) 2
2222
tff(axiom_modelet_is_exertable2, axiom,
23-
![M1: modelet, M2: modelet, T1: template, T2: template, E: engine]:
23+
![M1: modelet, M2: modelet, T1: template, T2: template, E: engine, R: requirement]:
2424
(
2525
(
2626
inputs_match(M1, T1)
2727
&
2828
inputs_match(M2, T2)
2929
&
3030
defines_input2(T1, T2, E)
31+
&
32+
(is_active(R) => engine_meets_requirement(E, R))
3133
)
3234
=>
3335
exertable2(E, M1, M2)
@@ -131,3 +133,24 @@ tff(axiom_engine_may_impart_property2, axiom,
131133
modelet_has_property(OM, P)
132134
)
133135
).
136+
137+
tff(axiom_engine_may_transit_property2, axiom,
138+
! [E: engine, IM1: modelet, IM2: modelet, OM: modelet, P: property]:
139+
(
140+
(
141+
exertable2(E, IM1, IM2)
142+
&
143+
exert2(E, IM1, IM2) = OM
144+
&
145+
engine_transits_property(E, P)
146+
&
147+
(
148+
modelet_has_property(IM1, P)
149+
|
150+
modelet_has_property(IM2, P)
151+
)
152+
)
153+
=>
154+
modelet_has_property(OM, P)
155+
)
156+
).

‎tff/tests/test-decision-engines.tff‎

Lines changed: 112 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
% Test Decision engines
2+
include('understanding-logic/tff/domains/decision-system/engines.tff').
3+
4+
5+
%%%%%% Input Modelets
6+
%---------------------------------------------------------------------------
7+
8+
%%% Alternatives (assume given for now)
9+
% A set of alternatives to choose from - the choice set.
10+
%-----------------------------------
11+
tff(given_alternatives_decl, type,
12+
given_alternatives_modelet : modelet
13+
).
14+
15+
tff(given_alternatives_modelet_creator, axiom,
16+
~?[E : engine]:
17+
modelet_has_creator(given_alternatives_modelet, E)
18+
).
19+
20+
%tff(given_alternatives_modelet_parents, axiom,
21+
% parents_of_modelet(given_alternatives_modelet) = empty_ms
22+
%).
23+
24+
% TODO: This cannot be a biconditional because other modelets (namely the choice/chosen set)
25+
% could also model the `alternative_array` concept
26+
tff(given_alternatives_modelet_models_alternative_array, axiom,
27+
(
28+
modelet_models_concept(given_alternatives_modelet, alternative_array)
29+
&
30+
![C : concept]:
31+
(
32+
modelet_models_concept(given_alternatives_modelet, C)
33+
=>
34+
C = alternative_array
35+
)
36+
)
37+
).
38+
39+
tff(given_alternatives_modelet_formalism, axiom,
40+
formalism_of_modelet(given_alternatives_modelet) = alternative_array_msg
41+
).
42+
43+
% TODO: This should probably not be a biconditional in general, but is fine for now.
44+
tff(given_alternatives_modelet_representation_class, axiom,
45+
![R : representation_class]:
46+
(
47+
modelet_has_representation_class(given_alternatives_modelet, R)
48+
<=>
49+
R = choice_set
50+
)
51+
).
52+
53+
%-----------------------------------
54+
55+
%%% Cues (assume given for now)
56+
% A set of cues to use to assess the alternatives.
57+
%-----------------------------------
58+
tff(given_cues_modelet_decl, type,
59+
given_cues_modelet : modelet
60+
).
61+
62+
tff(given_cues_modelet_creator, axiom,
63+
~?[E : engine]:
64+
modelet_has_creator(given_cues_modelet, E)
65+
).
66+
67+
%tff(given_cues_modelet_parents, axiom,
68+
% parents_of_modelet(given_cues_modelet) = empty_ms
69+
%).
70+
71+
% TODO: This should probably not be a biconditional in general, but is fine for now.
72+
tff(given_cues_modelet_models_cue_array, axiom,
73+
![C : concept]:
74+
(
75+
modelet_models_concept(given_cues_modelet, C)
76+
<=>
77+
C = cue_array
78+
)
79+
).
80+
81+
tff(given_cues_modelet_formalism, axiom,
82+
formalism_of_modelet(given_cues_modelet) = cue_array_msg
83+
).
84+
%-----------------------------------
85+
86+
87+
% Initial understanding
88+
%tff(initial_understanding_decl, type,
89+
% ius : modelet_set
90+
%).
91+
92+
%tff(initial_understanding_set_membership, axiom,
93+
% (
94+
% ![M : modelet]:
95+
% (
96+
% is_in_modelet_set(M, ius)
97+
% <=>
98+
% (
99+
% M = given_alternatives_modelet
100+
% |
101+
% M = given_cues_modelet
102+
% )
103+
% )
104+
% )
105+
%).
106+
107+
tff(input_modelets_are_distinct, axiom,
108+
$distinct(given_alternatives_modelet,
109+
given_cues_modelet)
110+
).
111+
112+
%---------------------------------------------------------------------------

0 commit comments

Comments
 (0)