adding decision logic

tff/domains/decision-system/properties.tff

@@ -0,0 +1,53 @@
+% Originally contributed by Tyler Olson  https://github.com/Rockjack00
+
+% Decision properties for fixed parameters
+%include('/understanding-logic/tff/model/properties.tff').
+
+%%%%%% Datatypes
+%---------------------------------------------------------------------------
+%%% Choice Size
+% TODO: This is not a datatype, it is a phenomenon.  but right now there's not a way to express that...
+%-----------------------------------
+tff(choice_size_datatype_decl, type,
+   choice_size_datatype : proptype
+).
+%-----------------------------------
+
+%---------------------------------------------------------------------------
+
+
+
+%%%%%% Properties
+%---------------------------------------------------------------------------
+%%% Decision Properties
+%-----------------------------------
+tff(absolute_size_prop_decl, type,
+   absolute_size_prop : property
+).
+
+tff(absolute_size_prop_datatype, axiom,
+  type_of_property(absolute_size_prop) = choice_size_datatype
+).
+
+%%% Choice properties
+%-----------------------------------
+tff(absolute_size_prop_decl, type,
+   absolute_size_prop : property
+).
+
+tff(n_parameter_prop_decl, type,
+   n_parameter_prop : property
+).
+
+tff(relation_parameter_prop_decl, type,
+   relation_parameter_prop : property
+).
+
+%-----------------------------------
+
+tff(properties_are_distinct, axiom,
+  $distinct(absolute_size_prop,
+            n_parameter_prop,
+            relation_parameter_prop
+            )
+).

tff/model/engines.tff

@@ -26,6 +26,11 @@ tff(decl_engine_output_properties, type,
 tff(decl_engine_imparts_output_properties, type,
   engine_imparts_output_property: (engine * property) > $o
 ).
+
+% Engine outputs may retain properties
+tff(engine_transits_property_decl, type,
+  engine_transits_property : (engine * property) > $o
+).
 %---
 
 tff(decl_engine_output_formalism, type,
@@ -79,13 +84,13 @@ tff(formally_equivalent, axiom,
         modelet_models_concept(M, C)
       )
       &
-%      ![R: representation_class]:
-%      ( % Equivalence of processing model classes
-%        template_has_representation_class_requirement(T, R)
-%        =>
-%        modelet_has_representation_class(M, R)
-%      )
-%      &
+      ![R: representation_class]:
+      ( % Equivalence of processing model classes
+        template_has_representation_class_requirement(T, R)
+        =>
+        modelet_has_representation_class(M, R)
+      )
+      &
       ! [SPT : spacetime_point]:
       (
         template_has_location_requirement(T, SPT)
@@ -137,3 +142,21 @@ tff(axiom_modelet_matches_template, axiom,
     inputs_match(M, T)
   )
 ).
+
+% Engines can conform to requirements
+tff(decl_engine_meets_requirement, type,
+  engine_meets_requirement: (engine * requirement) > $o
+).
+
+tff(axiom_engine_meets_requirement, axiom,
+  ! [E : engine, R : requirement, P: property]:
+  (
+    (
+      engine_has_property(E, P) % match engine to property
+      &
+      property_meets_requirement(P, R)
+    )
+    =>
+    engine_meets_requirement(E, R)
+  )
+).

tff/model/one.tff

@@ -20,12 +20,14 @@ tff(decl_exertable1, type,
 ).
 % Modelets are exertable by Engines (no sets) 1
 tff(axiom_modelet_is_exertable1, axiom,
-  ![M: modelet, T: template, E: engine]:
+  ![M: modelet, T: template, E: engine, R: requirement]:
   (
     (
       inputs_match(M, T)
       &
       defines_input1(T, E)
+      &
+      (is_active(R) => engine_meets_requirement(E, R))
     )
     =>
     exertable1(E, M)
@@ -132,3 +134,21 @@ tff(axiom_engine_may_impart_property1, axiom,
 ).
 
 
+
+tff(axiom_engine_may_transit_property1, axiom,
+  ! [E: engine, IM1: modelet, OM: modelet, P: property]:
+  (
+    (
+      exertable1(E, IM1)
+      &
+      exert1(E, IM1) = OM
+      &
+      engine_transits_property(E, P)
+      &
+      modelet_has_property(IM1, P)
+    )
+    =>
+    modelet_has_property(OM, P)
+  )
+).
+

tff/model/properties-and-requirements.tff

@@ -25,6 +25,9 @@ tff(decl_type_of_r, type,
 tff(decl_requirement_range, type,
   is_permissible: (requirement * $real) > $o).
 
+% Requirements can be active, when applied to engines
+tff(decl_requirement_active, type,
+  is_active: (requirement) > $o).
 
 tff(property_meets_requirement_decl, type,
   property_meets_requirement : (property * requirement) > $o

tff/model/sets.tff

@@ -222,6 +222,30 @@ tff(axiom_engine_may_impart_property, axiom,
   )
 ).
 
+%%%%%% Transitive properties
+%---------------------------------------------------------------------------
+% An engine transits a property from any of its inputs to its output.
+% That is if any of its inputs have some property P, then its output will also
+% have that property P.
+tff(axiom_engine_transits_property, axiom,
+  ![E : engine, P : property, MS : modelet_set]:
+  (
+    (
+      exertable(E, MS)
+      &
+      engine_transits_property(E, P)
+      &
+      ?[Mparent : modelet]:
+      (
+        is_in_modelet_set(Mparent, MS)
+        &
+        modelet_has_property(Mparent, P)
+      )
+    )
+    =>
+    modelet_has_property(exert(E, MS), P)
+  )
+).
 
 %Engines produce reliable output
 %tff(axiom_engine_reliability, axiom,

tff/model/three.tff

@@ -19,7 +19,7 @@ tff(decl_exertable3, type,
 ).
 % Modelets are exertable by Engines (no sets) 3
 tff(axiom_modelet_is_exertable3, axiom,
-  ![M1: modelet, M2: modelet, M3: modelet, T1: template, T2: template, T3: template, E: engine]:
+  ![M1: modelet, M2: modelet, M3: modelet, T1: template, T2: template, T3: template, E: engine, R: requirement]:
   (
     (
       inputs_match(M1, T1)
@@ -29,6 +29,8 @@ tff(axiom_modelet_is_exertable3, axiom,
       inputs_match(M3, T3)
       &
       defines_input3(T1, T2, T3, E)
+      &
+      (is_active(R) => engine_meets_requirement(E, R))
     )
     =>
     exertable3(E, M1, M2, M3)
@@ -133,3 +135,28 @@ tff(axiom_engine_may_impart_property3, axiom,
     modelet_has_property(OM, P)
   )
 ).
+
+
+
+tff(axiom_engine_may_transit_property3, axiom,
+  ! [E: engine, IM1: modelet, IM2: modelet, IM3: modelet, OM: modelet, P: property]:
+  (
+    (
+      exertable3(E, IM1, IM2, IM3)
+      &
+      exert3(E, IM1, IM2, IM3) = OM
+      &
+      engine_transits_property(E, P)
+      &
+      (
+        modelet_has_property(IM1, P)
+        |
+        modelet_has_property(IM2, P)
+        |
+        modelet_has_property(IM3, P)
+      )
+    )
+    =>
+    modelet_has_property(OM, P)
+  )
+).

tff/model/two.tff

@@ -20,14 +20,16 @@ tff(decl_exertable2, type,
 ).
 % Modelets are exertable by Engines (no sets) 2
 tff(axiom_modelet_is_exertable2, axiom,
-  ![M1: modelet, M2: modelet, T1: template, T2: template, E: engine]:
+  ![M1: modelet, M2: modelet, T1: template, T2: template, E: engine, R: requirement]:
   (
     (
       inputs_match(M1, T1)
       &
       inputs_match(M2, T2)
       &
       defines_input2(T1, T2, E)
+      &
+      (is_active(R) => engine_meets_requirement(E, R))
     )
     =>
     exertable2(E, M1, M2)
@@ -131,3 +133,24 @@ tff(axiom_engine_may_impart_property2, axiom,
     modelet_has_property(OM, P)
   )
 ).
+
+tff(axiom_engine_may_transit_property2, axiom,
+  ! [E: engine, IM1: modelet, IM2: modelet, OM: modelet, P: property]:
+  (
+    (
+      exertable2(E, IM1, IM2)
+      &
+      exert2(E, IM1, IM2) = OM
+      &
+      engine_transits_property(E, P)
+      &
+      (
+        modelet_has_property(IM1, P)
+        |
+        modelet_has_property(IM2, P)
+      )
+    )
+    =>
+    modelet_has_property(OM, P)
+  )
+).

tff/tests/test-decision-engines.tff

@@ -0,0 +1,112 @@
+% Test Decision engines
+include('understanding-logic/tff/domains/decision-system/engines.tff').
+
+
+%%%%%% Input Modelets
+%---------------------------------------------------------------------------
+
+%%% Alternatives (assume given for now)
+% A set of alternatives to choose from - the choice set.
+%-----------------------------------
+tff(given_alternatives_decl, type,
+  given_alternatives_modelet : modelet
+).
+
+tff(given_alternatives_modelet_creator, axiom,
+  ~?[E : engine]:
+    modelet_has_creator(given_alternatives_modelet, E)
+).
+
+%tff(given_alternatives_modelet_parents, axiom,
+%  parents_of_modelet(given_alternatives_modelet) = empty_ms
+%).
+
+% TODO: This cannot be a biconditional because other modelets (namely the choice/chosen set)
+%    could also model the `alternative_array` concept
+tff(given_alternatives_modelet_models_alternative_array, axiom,
+  (
+    modelet_models_concept(given_alternatives_modelet, alternative_array) 
+    &
+    ![C : concept]:
+    (
+      modelet_models_concept(given_alternatives_modelet, C) 
+      => 
+      C = alternative_array
+    )
+  )
+).
+
+tff(given_alternatives_modelet_formalism, axiom,
+  formalism_of_modelet(given_alternatives_modelet) = alternative_array_msg
+).
+
+% TODO: This should probably not be a biconditional in general, but is fine for now.
+tff(given_alternatives_modelet_representation_class, axiom,
+  ![R : representation_class]:
+  (
+    modelet_has_representation_class(given_alternatives_modelet, R) 
+    <=> 
+    R = choice_set
+  )
+).
+
+%-----------------------------------
+
+%%% Cues (assume given for now)
+% A set of cues to use to assess the alternatives.
+%-----------------------------------
+tff(given_cues_modelet_decl, type,
+  given_cues_modelet : modelet
+).
+
+tff(given_cues_modelet_creator, axiom,
+  ~?[E : engine]:
+    modelet_has_creator(given_cues_modelet, E)
+).
+
+%tff(given_cues_modelet_parents, axiom,
+%  parents_of_modelet(given_cues_modelet) = empty_ms
+%).
+
+% TODO: This should probably not be a biconditional in general, but is fine for now.
+tff(given_cues_modelet_models_cue_array, axiom,
+  ![C : concept]:
+  (
+    modelet_models_concept(given_cues_modelet, C)
+    <=>
+    C = cue_array
+  )
+).
+
+tff(given_cues_modelet_formalism, axiom,
+  formalism_of_modelet(given_cues_modelet) = cue_array_msg
+).
+%-----------------------------------
+
+
+% Initial understanding
+%tff(initial_understanding_decl, type,
+%  ius : modelet_set
+%).
+
+%tff(initial_understanding_set_membership, axiom,
+%  (
+%    ![M : modelet]:
+%    (
+%      is_in_modelet_set(M, ius)
+%      <=>
+%      (
+%        M = given_alternatives_modelet
+%        |
+%        M = given_cues_modelet
+%      )
+%    )
+%  )
+%).
+
+tff(input_modelets_are_distinct, axiom,
+  $distinct(given_alternatives_modelet, 
+            given_cues_modelet)
+).
+
+%---------------------------------------------------------------------------