1 /* MetaEthical.AI
 2    ==============
 3    Read the Introduction at:
 4    https://medium.com/@june_ku/formal-metaethics-and-metasemantics-for-ai-alignment-2e72533cad6d
 5 
 6    Developed by June Ku in the set theoretic programming language setlX v2.2.0
 7    and interspersed with considerable non-technical philosophical commentary.
 8      https://randoom.org/Software/SetlX/ 
 9      https://download.randoom.org/setlX/pc/archive/setlX_v2-2-0.binary_only.zip
10        - contains among other things, tutorial.pdf introduction and reference
11 
12    I am very grateful to Howard Nye for our work together on metaethics as well 
13    as many helpful comments and conversations during much of this development.
14    I also appreciate helpful discussions with Mahendra Prasad, Jessica Taylor, 
15    Anna Salamon and Nate Soares.
16 */
17 load('lib.stlx');
18 load('causal_model.stlx');
19 load('causal_markov_model.stlx');
20 load('decision_algorithm.stlx');
21 
22 /* MetaEthical.AI Utility Function
23    ===============================
24    Takes a causal markov model of the world w and set of brains bs in w and 
25    returns a metaethical.ai utility function. 
26 
27    Abstract: We construct a fully technical ethical goal function for AI by 
28    directly tackling the philosophical problems of metaethics and mental 
29    content. To simplify our reduction of these philosophical challenges into 
30    "merely" engineering ones, we suppose that unlimited computation and a 
31    complete low-level causal model of the world and the adult human brains in 
32    it are available.
33 
34    Given such a model, the AI attributes beliefs and values to a brain in two 
35    stages. First, it identifies the syntax of a brain’s mental content by 
36    selecting a decision algorithm which is i) isomorphic to the brain’s causal 
37    processes and ii) best compresses its behavior while iii) maximizing charity.
38    The semantics of that content then consists first in sense data that 
39    primitively refer to their own occurrence and then in logical and causal 
40    structural combinations of such content.
41 
42    The resulting decision algorithm can capture how we decide what to *do*, but 
43    it can also identify the ethical factors that we seek to determine when we 
44    decide what to *value* or even how to *decide*. Unfolding the implications 
45    of those factors, we arrive at what we should do. All together, this allows 
46    us to imbue the AI with the necessary concepts to determine and do what we 
47    should want it to do.  
48 */
49 metaethical_ai_u := procedure(w, bs) {
50   /* Given a set of brain models, associate them with the decision algorithms
51      they implement.  */
52   d := { [b, decision_algorithm.implemented_by(b, {})] : b in bs };
53   /* Then map each brain to its rational self's values (understood extensionally
54      i.e. cashing out the meaning of their mental concepts in terms of the 
55      world events they refer to).  */
56   ext_rufs := { [b, d[b].ext_ruf(w,b)] : b in bs };
57 
58   state_space := w.cm().poss_states();
59   b := first(bs);
60   probs := b.r[first(b.p)];
61   // Possible social choice utility functions
62   psc_us := choices({ {[state, r_i] : r_i in [1..#state_space] }
63                       : state in state_space });
64   sc_u := sort_set(psc_us, procedure(psc_u1, psc_u2) {
65                     return meai_psc_dist(psc_u1, ext_rufs, state_space, probs) <
66                            meai_psc_dist(psc_u2, ext_rufs, state_space, probs);
67                    })[1];
68   return sc_u;
69 };
70 
71   meai_psc_dist := procedure(psc_u, ext_rufs, state_space, probs) {
72     return +/ { ord_u_dist(card_u_to_ord_u(ext_ruf, state_space, probs),
73                            card_u_to_ord_u(psc_u,   state_space, probs) ) ** 2
74                 : ext_ruf in ext_rufs };
75   };
76 
77 /* MIT License
78    -----------
79    Copyright 2019 June Ku 
80 
81    Permission is hereby granted, free of charge, to any person obtaining a copy 
82    of this software and associated documentation files (the "Software"), to deal
83    in the Software without restriction, including without limitation the rights 
84    to use, copy, modify, merge, publish, distribute, sublicense, and/or sell 
85    copies of the Software, and to permit persons to whom the Software is 
86    furnished to do so, subject to the following conditions:
87 
88    The above copyright notice and this permission notice shall be included in 
89    all copies or substantial portions of the Software.
90 
91    THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 
92    IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 
93    FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 
94    AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 
95    LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING 
96    FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS 
97    IN THE SOFTWARE.
98 */

   1 class decision_algorithm(i, o, p, cp, u, m, m2, n, r, t_s, t_o,
   2                          cached_f, cached_lf, cached_ref) {
   3 // Definition and Structure of Decision Algorithms 
   4 // ===============================================
   5 
   6   i := i; /* Set of input variables (or technically names, ie strings)
   7                which are a subset of range(p)
   8              e.g. { 'P(I_1)', 'P(I_2)', 'P(I_3)' } 
   9              i.e. the agent's sense data. 
  10              Generally, p should include it, e.g. { ['I_1', 'P(I_1)'], ... }
  11   Technical footnote: There's some abuse of notation here. Each string like 
  12   'I_1' can depending on context be treated as:
  13     i) an individual constant term / object. A predicate expression in the 
  14        domain of p that has this string as an argument would be the 
  15        prototypical context illustrating this usage. Semantically, these would 
  16        refer to the brain events that implement them.  
  17     ii) a couple possibilities for this option: 
  18       a) a 0-ary predicate or sentential expression. It takes no inputs and 
  19          forms a proposition on its own. 
  20       b) shorthand for a 1-place predicate that takes the constant in ii and 
  21          simply asserts its existence, perhaps loosely inspired by Free Logic's
  22          E!. 
  23       In either case, its truth-maker/referent would be the same as option i's.
  24       Treating the string as a sentential expression or forming an expression 
  25       with it as the argument of a connective would indicate this usage.  
  26     All of these possibilities are expressions, or terms that could figure in an
  27     expression, i.e. the sort of thing that would be in the domain of p. They 
  28     should be distinguished from the set i, which would be a subset of the range
  29     of p. These would be names of a decision algorithm variable, e.g. parents() 
  30     of other variables. Assignments of value to this variable would be a 
  31     subjective probability 0-1. That would form a local/partial decision state,
  32     which could get mapped to by a local/partial implementation functor lf() 
  33     from a local brain state.  */
  34 
  35   o := o; /* Set of output variables
  36              e.g. { 'O_1', 'O_2', 'O_3' }
  37              i.e. the agent's motor output. 
  38              See also the technical note for i.  */
  39 
  40   /* Function from logical formulas (setlx functors/strings/terms) to 
  41        probability variables
  42      e.g. { ['A', 'P(A)'], ['B', 'P(B)'], [And('A', 'B'), 'P(A & B)'], 
  43             [BoxArrow('A', 'B'), 'P(A []-> B)'] }  */
  44   p := p;
  45 
  46   /* Function from ordered pairs [x, y] to conditional probability variables
  47      e.g. { [[x, y], 'P(x|y)'], ... } 
  48      or more concretely: { [['C', And('A', 'B')], 'P(C|A,B)'], ... }  */
  49   cp := cp;
  50 
  51   /* Function from logical formulas to utility variables 
  52        e.g. { ['A', 'U(A)'], ... } 
  53      u has the same structure as p above.
  54      See also accepted norms / higher-order utilities a few lines below. */
  55   u := u;
  56 
  57   /* Set of memory variables 
  58      This is a catch-all for other cognitive states that don't fit into the 
  59      other sets of variables yet may be important to model, e.g. intermediate 
  60      states in a calculation performing inference or decision. One can think of
  61      it as roughly analogous to a computer's RAM.  */
  62   m := m;
  63 
  64   /* Set of memory variables for t_o 
  65      Same idea as m above but these only mediate between p + cp + u and o. 
  66      This helps ensure it is a genuinely decision algorithmic explanation.  */
  67   m2 := m2;
  68 
  69   /* List of accepted norms / higher-order utilities
  70      [ n_1, n_2, ... ]
  71      each n_i == { ['e', e_n_i], ['m2', m2_n_i], ['o', o_n_i] }
  72        e_n_i is a function from logical formulas to evaluation variables
  73          e.g. { ['A', 'E_n_i(A)'], ... }
  74          They are basically utility function variables but since they are
  75          higher-order, i.e. they influence normative judgments or prescriptions
  76          rather than motor output, we call them evaluation variables instead
  77          when we want to emphasize that they don't directly govern action.
  78        m2_n_i is a set of memory variables that only moderate p + e_n_i to 
  79          o_n_i
  80        o_n_i is a set of output variables that causally influence various u or
  81          e_n_j. In simplified models, we can make o_n_i trivially cause u or 
  82          e_n_i states by just being identical to them 
  83 
  84      These are essentially decision criteria that govern how we change our
  85      preferences or other higher-order norms. The way in which they govern is 
  86      analogous and mathematically isomorphic to how first-order utility 
  87      functions or preferences govern action. There, beliefs that some motor
  88      output would cause some preferred state to be achieved will tend to cause
  89      such output and therefore the desired state. In the case of these accepted
  90      norms, beliefs that the output variables (which we can also understand as 
  91      normative judgments or prescriptions) will cause or constitute a change 
  92      in values (which is what the exprs of the domain of e_n_i would refer to) 
  93      will tend to cause such outputs and therefore changes in value. 
  94 
  95      It is very important to note that what makes these preferences / utilities 
  96      higher-order is their causal or functional roles and not the content of 
  97      the expressions associated with the evaluation variables. One can have, in 
  98      our sense, first-order preferences which prefer states involving other
  99      preferences. Those might be referentially "higher-order" in some sense but 
 100      they would still be first-order in our sense so long as they govern
 101      actions rather than normative judgments or prescriptions.
 102 
 103      See http://www.metaethical.ai/norm_descriptivism.pdf for more.
 104 
 105      One might object that introducing these higher-order utility functions
 106      invalidates what was supposed to be the utility function of the decision
 107      algorithm. Since a utility function is supposed to encompass any factors   
 108      explaining behavior, wouldn't it already include these allegedly
 109      higher-order factors? Strictly speaking, that may be correct, but that kind
 110      of utility function is not the most useful for our purposes.
 111      
 112      It may be better to think in terms of modeling a decision algorithm as a
 113      society of subagents. The first-order utility function then is the utility
 114      function of the subagent whose outputs are the decision algorithm's actions
 115      rather than prescriptions that directly influence other subagents' 
 116      utilities. When we speak of the utility function of the decision algorithm,
 117      this should just be understood as shorthand for this first-order utility 
 118      function.
 119   */
 120   n := n;
 121 
 122   // Internal states
✔ 123   s := procedure() {
 124     if (n == {} || n == [] || n == om) {
 125       n_vs := {};
 126     } else {
 127       n_vs := +/ { range(n_i['e']) + n_i['m2'] + n_i['o'] : n_i in n };
 128     }
 129     return range(p) + range(cp) + range(u) + m + m2 + n_vs - i;
 130   };
 131 
 132   // Function from i + s() + o to ranges of values for those variables
 133   r := r;
 134 
 135   /* Higher order function from a function assigning values to all input and 
 136      internal states to a function assigning values to all next internal states 
 137        is -> s
 138   */
 139   t_s := t_s;
 140 
 141   /* Higher order function from a function assigning values to all probability 
 142      and utility variables as well as m2 to a function assigning values to 
 143      outputs 
 144        p u m2 -> o
 145   */
 146   t_o := t_o;
 147 
 148   /* State transitions
 149      Returns a higher-order function from functions assigning values to i + s 
 150      to functions assigning values to s + o. This is the intuitive combination
 151      of t_s and t_o. */
✔ 152   t := procedure() {
 153     return { [    // a higher-order function which takes 
 154               is, // a function assigning values to i + s and returns a function
 155               t_s[is] + t_o[just_p_u_m2(is)]
 156                   // composed of the union of a func assigning values to s and 
 157                   // a func assigning values to o
 158              ] : is in domain(t_s) };
 159   };
 160 
 161   /* We explicitly cache f after computing it. This allows us to directly set
 162      its value when testing or when performing the brute force search would be
 163      prohibitively costly.  */
 164   cached_f := cached_f;
 165   cached_lf := cached_lf;
 166 
 167   /* ns as in the plural of n. 
 168      Takes 'e', 'm2' or 'o' and returns the corresponding variables from all n.
 169      e.g. ns('e') would return all e_n_i */
✔ 170   ns := procedure(str) {
 171     if (str == 'e') {
 172       return +/ { range(n_i[str]) : n_i in n };
 173     } else {
 174       return +/ { n_i[str] : n_i in n };
 175     }
 176   };
 177 
✔ 178   p_vars := procedure() {
 179     return range(p) + range(cp);
 180   };
 181 
✔ 182   p_u_vars := procedure() {
 183     return p_vars() + range(u);
 184   };
 185 
 186   /* Takes a function (is) assigning values to input and internal state vars
 187      and returns its partial function with only vars in p, u and m2  */
✔ 188   just_p_u_m2 := procedure(is) {
 189     return { [var, val] : [var, val] in is | var in p_u_vars() + m2 };
 190   };
 191 
 192 // Variable Relationships 
 193 // ----------------------
 194 
 195   /* Takes a variable and returns its parents, i.e. the variables that 
 196      are necessary to determine its next state in the state transition t(). */
✔ 197   parents := procedure(y) {
 198     result := { z : z in (i + s()) | is_necessary_parent_of(z, y) };
 199     return result;
 200   };
 201 
✔ 202     is_necessary_parent_of := procedure(z, y) {
 203       vs := {v : v in i + s() | v != z}; // all other variables but z
 204       f_vs := possible_states(vs, r);
 205       bool := exists(f_v in f_vs | vals_diff(f_v, y, z));
 206       return bool;
 207     };
 208 
 209     /* Check whether there exists an assignment of values to the other 
 210        variables such that there are still different values of y depending 
 211        on values of z.  */
✔ 212     vals_diff := procedure(f_v, y, z) {
 213       vals := { t_s[ f_v + {[z,r_i]} ][y] : r_i in r[z] };
 214       return #vals > 1;
 215     };
 216 
 217   // Takes a variable and returns its children
✔ 218   children := procedure(y) {
 219     return { v : v in s() + o | y in parents(v) };
 220   };
 221 
 222   /* Takes a variable v and a set of variables vs (with v usually in vs)
 223      and returns the first ancestors within any given branch of v's ancestors 
 224      that are not in vs */
✔ 225   non_shared_ancestors := procedure(v, vs) {
 226     result := {};
 227     for (parent in parents(v)) {
 228       if (parent in vs) {
 229         result := result + non_shared_ancestors(parent, vs);
 230       } else {
 231         result := result + { parent };
 232       }
 233     }
 234     return result;
 235   };
 236 
 237   /* Takes a variable v and a set of variables vs (with v usually in vs)
 238      and returns the first descendants within any given branch of v's 
 239      descendants that are not in vs */
✔ 240   non_shared_descendants := procedure(v, vs) {
 241     result := {};
 242     for (child in children(v)) {
 243       if (child in vs) {
 244         result := result + non_shared_descendants(child, vs);
 245       } else {
 246         result := result + { child };
 247       }
 248     }
 249     return result;
 250   };
 251 
 252 
 253 // Syntax and Implementation
 254 // =========================
 255 // See also better_explanation and the section starting with complexity.
 256 
 257   /* Function from a causal_markov_moodel of a brain to an implementation 
 258      mapping f which is a higher-order function from a function assigning 
 259      states to the brain's variables to a function assigning states to internal 
 260      state variables s() meeting certain criteria. 
 261   */
 262   f := procedure(b) {
 263     if (cached_f == om) {
 264       cached_f := compute_f(b);
 265     }
 266     return cached_f;
 267   };
 268 
 269   compute_f := cachedProcedure(b) {
 270     fs := { pf : pf in possible_fs(b) | commutes(pf, b) };
 271     /* Todo: Sort by complexity and return the simplest? 
 272        Or also factor in ambitiousness? Coverage of more states?  */
 273     if (#fs > 0) {
 274       return first(fs);
 275     } else {
 276       return {};
 277     }
 278   };
 279 
 280   /* Function from a causal_markov_model of a brain to the possible 
 281      implementation mappings f which map from a function assigning values to 
 282      the exogenous and endogenous variables of the causal_markov_model to 
 283      functions assigning values to the input, internal state, and output 
 284      variables. */
 285   possible_fs := procedure(b) {
 286     return function_space( b.poss_states(), poss_states() );
 287   };
 288 
✔ 289   poss_states := cachedProcedure() {
 290     return possible_states(i + s() + o, r);
 291   };
 292 
✔ 293   is_implemented_by := procedure(b) {
 294     return !(f(b) == {});
 295   };
 296 
 297   /* Implementation Functor
 298      ----------------------
 299      Check whether a possible implementation functor pf commutes. See f.
 300 
 301      This basically implements Chalmers' criterion for when some causal system 
 302      implements a computation: http://consc.net/papers/rock.html
 303 
 304      In category theory terms, we can say that f is an implementation functor.
 305      Given a category of brain states and the causal relations between them
 306      and another of decision states and cognitive state transitions between
 307      them, f would be a functor mapping i) brain states to decision states and
 308      ii) causal transitions to decision state transitions such that it doesn't
 309      matter whether one goes from a) a brain state to the brain state it causes 
 310      and then to the decision state f maps that brain state to or b) first from 
 311      the same original brain state to the decision state f says it implements 
 312      and then to the next decision state this decision algorithm transitions to.
 313      Either way, you would end up at the same final decision state. 
 314   */
✔ 315   commutes := procedure(pf, b) {
 316     /*                 pf
 317       bs_{b.uv_t_i-1} ------> ds_iso_t_i-1
 318        |                       |
 319        | b.response            | restrict_domain
 320        |                       | t()
 321        v                       v
 322       bs_{b.v_ti} ----------> ds_so_t_i
 323            +u  pf  restrict_domain
 324 
 325       Roughly check that t( pf ) == pf( b.response ) 
 326     */
 327     return forall(bs in domain(pf) |
 328        t()[restrict_domain(pf[bs], i + s())] ==
 329        restrict_domain(pf[
 330          b.response(b.v, bs) + { [u_var, first(b.r[u_var])] : u_var in b.u }
 331        ], s() + o)
 332      );
 333   };
 334   /* Technical footnote: The above is almost true, but causal response and 
 335      decision state transitions don't quite take brain states to entire brain 
 336      states or entire decision states to entire decision states. The causal 
 337      response only specifies the endogenous variables on the next time step. So 
 338      in order to have a full brain state for pf, we just fill in the exogenous 
 339      variables with their first values, only to drop those values anyway after
 340      obtaining the decision state it implements. Similarly, with the decision 
 341      state, the previous outputs are irrelevant to the state transition to the 
 342      next decision state so we drop those before finding the next decision 
 343      state which is almost full with the exception of the (exogenous) inputs.
 344 
 345      The code should be correct and this only affects the intuitive explanation.
 346      If we had used lf which is defined below, I think we could truly say it is
 347      a functor. Since it maps partial brain states to (sets of) partial 
 348      decision states, it wouldn't need to make the aforementioned adjustments
 349      which prevent it from quite being a functor. However, lf is defined in 
 350      terms of f, so we'd still need to understand f first and for now, 
 351      almost-a-functor might have to do.
 352   */
 353 
 354   /* Takes a decision state assigning values to i + s() + o and returns a
 355      function assigning values to just s() + o  */
✔ 356   drop_i := procedure(ds) {
 357     return { [var, val] : [var, val] in ds | !(var in i) };
 358   };
 359 
 360   /* Local / partial f
 361      Returns a function mapping partial causal states to partial decision states
 362      which commutes, i.e. it maps partial causal states to the partial decision 
 363      state which is forced by the complete mapping f.  */
 364   lf := procedure(b) {
 365     if (cached_lf == om) {
 366       cached_lf := compute_lf(b);
 367     }
 368     return cached_lf;
 369   };
 370 
 371   compute_lf := cachedProcedure(b) {
 372     /* Possible local fs 
 373        Function space from union of partial causal states to the union of 
 374        partial decision states.  */
 375     plfs := function_space(
 376       +/ { partial_functions(cs) : cs in b.poss_states() }, // causal states
 377       +/ { partial_functions(ds) : ds in poss_states() } // decision states
 378     );
 379     lfs := [ plf : plf in plfs | lf_commutes(plf, b) ];
 380     lfs := sort_list(lfs, procedure(plf1, plf2) { return #plf1 > #plf2; });
 381     return lfs[1];
 382   };
 383 
 384   /* Function from possible local function plf and a causal model of brain b 
 385      to boolean value whether it commutes. */
✔ 386   lf_commutes := procedure(plf, b) {
 387     return forall(pcs in domain(plf) |  // pcs = partial causal state
 388       /* The set of complete decision states that is mapped by f from each 
 389          complete causal state compatible with the partial causal state is 
 390          equal to the set of complete decision states compatible with 
 391          the partial decision states mapped by the possible lf from the partial
 392          causal state. */
 393       { f(b)[ccs] : ccs in compatible_complete_states(pcs, b.poss_states()) } ==
 394       compatible_complete_states(plf[pcs], poss_states())
 395     );
 396   };
 397 
 398   /* Local / partial f inverse
 399   /* Returns a "function" from local / partial decision states to a set of 
 400      local / partial causal states, namely the inverse of lf.  */
✔ 401   lf_inv := cachedProcedure(b) {
 402     return { [ds, { cs : cs in domain(lf(b)) | lf(b)[cs] == ds} ] :
 403              ds in range(lf(b)) };
 404   };
 405 
 406   // Helper function. Same as lf_inv but time subscripts are added to the b vars
✔ 407   lf_inv_at := procedure(b, t_i) {
 408     return { [ds, { assign_time(cs, t_i) : cs in css }]
 409              : [ds, css] in lf_inv(b) };
 410   };
 411 
 412   /* Takes an event in b.cm() and returns the local decision state that the 
 413      brain state implements.  */
✔ 414   lf_cm := procedure(b, b_event) {
 415     return lf(b)[drop_time(b_event)];
 416   };
 417 
 418   // Returns the decision state variables implemented by a local brain state.
✔ 419   lf_cm_vs := procedure(b, b_event) {
 420     d_event := lf_cm(b, b_event);
 421     if (d_event == om) {
 422       return {};
 423     } else {
 424       return domain(d_event);
 425     }
 426   };
 427 
 428   /* Similar to above but returns the formula in the domain(p) that gets 
 429      mapped to the p var.  */
✔ 430   lf_cm_p_inv := procedure(b, b_event) {
 431     vs := lf_cm_vs(b, b_event);
 432     if (#vs == 1) {
 433       return p_inv(first(vs));
 434     } else {
 435       return om;
 436     }
 437   };
 438 
✔ 439   plf_to_pf := procedure(b, plf) {
 440     /* For each decision state var, construct the function from complete 
 441        causal states to the state of that variable. */
 442     pf_var := {
 443       [var, +/ { { [ccs, pds]
 444                    : ccs in compatible_complete_states(pcs, b.poss_states())
 445                  } : [pcs, pds] in plf | first(first(pds)) == var }
 446       ] : var in i + s() + o
 447     };
 448     return { [bs, +/ { (pf_var[var])[bs] : var in i + s() + o }]
 449              : bs in b.poss_states() };
 450   };
 451 
 452 
 453   // This is mostly just checking for syntactic validity or well-formedness.
 454   // See also all_lte.
 455   is_valid := procedure() {
 456     return m2s_are_valid() && no_e_in_u();
 457   };
 458 
 459   /* Ensures that m2s merely moderate between p + u and o.
 460      I'm no longer sure if this is necessary since we measure and punish 
 461      attributing irrationality but it also doesn't seem too bad of a 
 462      simplifying assumption for now.  */
✔ 463   m2s_are_valid := procedure() {
 464     return forall (m2_i in m2 |
 465       forall (v in non_shared_ancestors(m2_i, m2) | v in p_u_vars()) &&
 466       forall (v in non_shared_descendants(m2_i, m2) | v in o)
 467     ) && forall (n_i in n |
 468       forall (m2_j_n_i in n_i['m2'] |
 469         forall (v in non_shared_ancestors(m2_j_n_i, n_i['m2']) |
 470                 v in p_vars() + range(n_i['e']) ) &&
 471         forall (v in non_shared_descendants(m2_j_n_i, n_i['m2']) |
 472                 v in n_i['o'])
 473       )
 474     );
 475   };
 476 
 477   /* This helps ensure higher-order ambitiousness by preventing the smuggling
 478      of evaluation functions within u. For each p expr of the form x []-> y,
 479      make sure it does not take the form that x-ing would bring about y which 
 480      the agent values (but x is not in the normal outputs o) and this 
 481      recognition causes x-ing. If it is of that form, we want a decision 
 482      algorithm that includes that explicitly within n.  
 483      Todo: Generalize to no_e_in_e and cover more cases, e.g. indirect 
 484      reference or equivalent expressions or influencing as grandparents.  */
 485   no_e_in_u := procedure() {
 486     return forall(expr in domain(p) | fct(expr) != "BoxArrow" || !e_in_u(expr));
 487   };
 488 
 489     e_in_u := procedure(expr) {
 490       x := args(expr)[1]; // like an n[i]['o']
 491       y := args(expr)[2];
 492       return y in domain(u) && !(x in o) && p[expr] in parents(x);
 493     };
 494 
 495 // Semantics of Mental Content 
 496 // ===========================
 497 
 498   /* Takes a set of pairs [w, b] and returns a function from possible worlds 
 499      to extensions / referents. 
 500        See: https://plato.stanford.edu/entries/two-dimensional-semantics/ 
 501   */
 502   intension := procedure(poss_wbs) {
 503     return { [wb[1], ref(wb[1], wb[2])] : wb in poss_wbs };
 504   };
 505 
 506   /* Reference
 507      ---------
 508      Reference function from causal markov model of world w and brain b 
 509      to a function which takes a brain and returns its set of truth-makers if 
 510      any, i.e. a set of poss events in the world or equivalently, functions
 511      assigning values to vars in the world. 
 512 
 513      There are a few ways that reference is grounded.
 514 
 515        1. Input variable states refer to the brain states implementing them.
 516           You can think of their content as something like "this sense datum
 517           is occurring" or perhaps even as just the pure demonstrative "this".
 518           It seems intuitive that these states can represent themselves since
 519           everything trivially carries information about itself. 
 520 
 521        2. The meanings of logical connectives (e.g. And, Or, Implies) and the 
 522           causal connective BoxArrow are grounded by the axioms that define 
 523           them. These meanings are enforced by punishing any attributions of 
 524           these connectives into credences that violate their axioms. See 
 525           incoherence. Cf inferential / conceptual role semantics:
 526             https://plato.stanford.edu/entries/content-narrow/#rol  
 527 
 528        3. The rest can be understood as a kind of ramsification. Other posited 
 529           objects/events, predicates and relations refer to those things
 530           (if any) which play the roles posited for them. 
 531              https://en.wikipedia.org/wiki/Ramsey%E2%80%93Lewis_method
 532              http://www.jimpryor.net/teaching/courses/mind/notes/ramseylewis.html
 533           We soften the requirement of strict truth by scoring by squared error.
 534           This amounts to a principle of charity favoring interpretations
 535           that make more beliefs turn out to be true (while also adhering to
 536           the constraints above).  
 537   */
 538   ref := procedure(w, b) {
 539     if (cached_ref == om) {
 540       cached_ref := compute_ref(w, b);
 541     }
 542     return cached_ref;
 543   };
 544 
 545   compute_ref := cachedProcedure(w, b) {
 546     /* Base expressions are strings or predicates. We'll build composite 
 547        expressions together with corresponding references out of combinations of
 548        these and logical / causal connectives. */
 549     base_exprs := { [expr, e_arity] : [expr, e_arity] in str_exprs() + preds()
 550                                     | !(p[expr] in i) };
 551     pbers := poss_base_expr_refs(w, base_exprs);
 552     poss_atom_refs := { i_ref(w, b) + base_ref
 553                         : base_ref in poss_base_refs(w, b, pbers) };
 554     poss_refs := [ full_ref(w, b, poss_atom_ref)
 555                    : poss_atom_ref in poss_atom_refs ];
 556     return sort_list(poss_refs, less_sq_err)[1];
 557   };
 558 
 559     /* Input vars refer to their own brain-state implementors. */
 560     i_ref := procedure(w, b) {
 561       return {
 562         [b_event, compatible_complete_states(b_event, w.cm().poss_states())]
 563         : b_event in b.actual_sync_events()
 564         | #lf_cm(b, b_event) == 1 && lf_cm(b, b_event) in poss_i_events()
 565       };
 566     };
 567 
✔ 568     str_exprs := procedure() {
 569       return { [expr, 0] : expr in domain(p)
 570                          | !(p[expr] in i) && isString(expr) };
 571     };
 572 
✔ 573     preds := procedure() {
 574       return { [fct(expr), arity(expr)]
 575                : expr in domain(p)
 576                | isTerm(expr) && !(fct(expr) in connectives()) };
 577     };
 578 
 579     // Set of choices of poss assignments of world w states/sets/tuples to expr
✔ 580     poss_base_expr_refs := procedure(w, base_exprs) {
 581       return choices({ {expr} >< range_for_arity(e_arity, w.cm().poss_states())
 582                        : [expr, e_arity] in base_exprs });
 583     };
 584 
 585     /* Use poss_base_expr_refs to construct poss reference functions assigning
 586        reference to brain events rather than exprs.  */
 587     poss_base_refs := procedure(w, b, pbers) {
 588       return {
 589         +/ {
 590           // For each brain event that represents the given expr
 591           // Assign to it the reference of that expr according to pber
 592           { [b_event, pber[expr]] : b_event in b.actual_sync_events()
 593                                   | lf_cm_p_inv(b, b_event) == expr }
 594           // Do that for each base expr and collect them into a single function
 595           : expr in domain(pber) }
 596         // for each poss base expr reference func
 597         : pber in pbers
 598       };
 599     };
 600 
 601     // Full Reference
 602     // Much of the below builds on fairly standard first-order structures or 
 603     // models, e.g., https://en.wikipedia.org/wiki/First-order_logic#Semantics 
 604     full_ref := procedure(w, b, atom_ref) {
 605       /* Full ref maps each brain event which implements a credence to the 
 606          result of reducing the reference of the corresponding expression. */
 607       return { [b_event, rr(
 608                             lf_cm_p_inv(b, b_event), // expr it is credence in 
 609                             [ w, b, atom_ref,
 610                               // vars are all the same time so just take 1st
 611                               var_time(first(first(b_event))),
 612                               {} ] // empty context
 613                          ) ]
 614                : b_event in actual_p_events(b) };
 615     }; // end full_ref
 616 
 617       /* Reduce reference, takes an expression and an array of further
 618          parameters consisting of a world, brain, atomic reference function, 
 619          time and context and returns a set of truth-making w events or the set 
 620          of w events the expression is true in. The set of truthmakers is our 
 621          way of enforcing a canonical boolean algebraic form. The different 
 622          elements act as disjuncts of events and combining assignments of vals 
 623          to vars into a map acts as conjunction. It may seem counterintuitive 
 624          and take some getting used to but we use this canonical form even when
 625          there there is only one disjunct. */
✔ 626       rr := procedure(expr, arr) {
 627         w := arr[1]; b := arr[2]; atom_ref := arr[3]; ti := arr[4];
 628         context := arr[5];  // context is for binding of variables, see Exists
 629         if (isTerm(expr)) {
 630           if (#args(expr) >= 1) { a1 := args(expr)[1]; }
 631           if (#args(expr) >= 2) { a2 := args(expr)[2]; }
 632         }
 633         switch {
 634           case expr in domain(context) :
 635             return context[expr];
 636           case p[expr] in i :
 637             return compatible_complete_states(
 638                      first({ b_event : b_event in pow(b.a[ti])
 639                                      | lf_cm_p_inv(b, b_event) == expr }),
 640                      w.cm().poss_states()
 641                    );
 642           case isString(expr) :
 643             return atom_ref[expr];
 644           case isSet(expr) :
 645             /* This shouldn't happen but just in case, return the set.
 646                Maybe throw an error instead? Or it's probably just rr(rr(.. */
 647             print('Warning: Expected an expr but received a set: ' + expr);
 648             return expr;
 649           case fct(expr) == 'At_t' :
 650             if (ti + a2 >= 0) { // a2 should already be negative
 651               return rr(a1, [w, b, atom_ref, ti + a2, context]);
 652             } else {
 653               return {};
 654             }
 655           case fct(expr) == 'And' :
 656             return rr(a1, arr) * rr(a2, arr);
 657           case fct(expr) == 'Or' :
 658             return rr(a1, arr) + rr(a2, arr);
 659           case fct(expr) == 'Not' :
 660             return w.cm().poss_states() - rr(a1, arr);
 661           case fct(expr) == 'Implies' :
 662             return rr( Or(Not(a1), a2), arr );
 663           case fct(expr) == 'Forall' :
 664             // Vx Px = ~Ex ~Px
 665             return rr(Not(Exists(a1, Not(a2))), arr);
 666           case fct(expr) == 'Exists' :
 667             // Set of truth-makers for a2 when any {w_event} is subbed for a1
 668             return +/ { rr(a2, [ w, b, atom_ref, ti,
 669                                  context + { [a1, {w_event}] } ])
 670                         : w_event in range_for_arity(0, w.cm().poss_states()) };
 671           case fct(expr) == 'BoxArrow' : // A []-> B, subjunctive conditional
 672             // Antecedent
 673             if (isSet(a1)) {
 674               ant := a1;
 675             } else {
 676               ant := states2events(rr(a1, arr));
 677             }
 678             // Consequent
 679             if (isSet(a2)) {
 680               cons := a2;
 681             } else {
 682               cons := states2events(rr(a2, arr));
 683             }
 684             if (#ant > 1) { // Antecedent has disjuncts.
 685               // This or that causes the effect if this does or that does.
 686               return +/ { rr(BoxArrow(disjunct, cons), arr) : disjunct in ant };
 687             } else if (#ant == 1) {
 688               if (#cons > 1) {
 689                 // A thing causes this or that if it causes this or causes that.
 690                 return +/ { rr(BoxArrow(ant, disjunct), arr) : disjunct in cons };
 691               } else if (#cons == 1) {
 692                 if ( w.cm().response( domain(cons[1]), ant[1] ) == cons[1] ) {
 693                   /* If this aspect of the causal model is true, it's true in
 694                      all states. Fire causes smoke can be true even in a     
 695                      possible world where all fire is prevented. A more 
 696                      expressive language could substitute a more meaningful 
 697                      truthmaker here. */
 698                   return w.cm().poss_states();
 699                 } else {
 700                   return {};
 701                 }
 702               } else {
 703                 // Trivially true because everything causes the empty effect? 
 704                 return w.cm().poss_states();
 705               }
 706             } else {
 707               return {}; // Nothing is caused by nothingness?
 708             }
 709             return om;
 710           default : // Predicate or Relation
 711             tuple := [rr(arg, arr) : arg in args(expr)];
 712             if (tuple in atom_ref[fct(expr)]) {
 713               // If a predication is true, it's true in all states.
 714               return w.cm().poss_states();
 715             } else {
 716               return {};
 717             }
 718         } // end switch
 719       }; // end rr
 720 
 721     less_sq_err := procedure(w, b, ref_1, ref_2) {
 722       return sq_err(w, b, ref_1) < sq_err(w, b, ref_2);
 723     };
 724 
✔ 725     sq_err := procedure(w, b, ref_i) {
 726       return +/ {
 727         ( true_p(w, ref_i, b_event) - first(range(lf_cm(b, b_event))) ) ** 2
 728         : b_event in actual_p_events(b)
 729       };
 730     };
 731 
✔ 732     true_p := procedure(w, ref_i, b_event) {
 733       if (w.actual_state() in ref_i[b_event]) {
 734         return 1;
 735       } else {
 736         return 0;
 737       }
 738     };
 739 
 740   // Takes an expression (in a world, brain and time) and returns its referent.
✔ 741   ref_expr := procedure(w, b, t_i, expr) {
 742     p_var := p[expr];
 743     ds := f(b)[drop_time(b.a[t_i])]; // decision state
 744     p_event := { [p_var, ds[p_var]] };
 745     b_event := first( lf_inv_at(b, t_i)[p_event] );
 746     return ref(w, b)[b_event];
 747   };
 748 
 749   // Returns the brain events that implement a placement of probabibility.
✔ 750   actual_p_events := procedure(b) {
 751     return { b_event : b_event in b.actual_sync_events()
 752              |      #lf_cm_vs(b, b_event) == 1 &&         // just one var
 753                first(lf_cm_vs(b, b_event)) in range(p) }; // and it's a p_var
 754   };
 755 
 756   /* Function from causal_markov_model b to a function from times to 
 757      probability states, i.e. assignments of values to range(p) + range(cp).
 758      At each time, use f(b) to see what decision state it maps the 
 759      brain state to and collect the states for range(p) + range(cp). 
 760 
 761      Actual world b.a is a function from times to assignments of values to 
 762      variables at that time.
 763         e.g. b.a := { [1, assign_time({ [y, true] : y in b.uv() }, 1)], ...} */
✔ 764   prob_states := procedure(b) {
 765     return { [ti, prob_states_t(b, ti) ] : ti in [1..b.n] };
 766   };
 767 
 768   /* Probability States at Time ti 
 769      Takes a brain b at a time ti and returns the decision state that is 
 770      implemented by that brain state but restricted to just the probability 
 771      variables.  */
✔ 772   prob_states_t := procedure(b, ti) {
 773     bs := { [var, val] : [var, val] in drop_time(b.a[ti]) | var in b.uv() };
 774     ds := f(b)[bs];
 775     return { [var, val] : [var, val] in ds | var in p_vars() };
 776   };
 777 
 778 
 779 // Utility / Evaluation Functions
 780 // ==============================
 781 
 782   // Collect all utility/evaluation function vars with their output vars
✔ 783   eo := procedure() {
 784     return {[u, o]} + { [n_i['e'], n_i['o']] : n_i in n };
 785   };
 786 
 787   /* Instrumental irrationality, including of evaluation as well as utility 
 788      functions. */
✔ 789   instr_irrat := procedure(w, b) {
 790     return +/ { e_dist(w, b, ti) : ti in [1..(b.n - 1)] } / (b.n - 1);
 791   };
 792 
 793     /* Takes a brain b and time ti and returns the distance between the actual 
 794        outputs and the optimal outputs according to the utility / evaluation 
 795        functions and []-> beliefs.  */
 796     e_dist := procedure(w, b, ti) {
 797       /* These are all weighted equally right now, but we may want to 
 798          consider different weights. Should first-order utility be treated 
 799          differently? What about highest order? Does complexity matter?  */
 800       return +/ { e_i_dist(w, b, ti, e_i, o_i) : [e_i, o_i] in eo() } / #eo();
 801     }; // end e_dist
 802 
 803     // Similar to above but for a specific util/eval function and output vars
 804     e_i_dist := procedure(w, b, ti, e_i, o_i) {
 805       poss_o_i_states := possible_states(o_i, r);
 806       actual_d_st0 := f(b)[ drop_time(b.a[ti]  ) ];
 807       actual_d_st1 := f(b)[ drop_time(b.a[ti+1]) ];
 808       actual_o_i_state := { [o_i_j, actual_d_st1[o_i_j]] : o_i_j in o_i };
 809       sorted_o_i_states := sort_list( [x : x in poss_o_i_states],
 810         procedure(x, y) {
 811           return exp_u(w, b, ti, actual_d_st0, e_i, x) >
 812                  exp_u(w, b, ti, actual_d_st0, e_i, y);
 813         } );
 814       ix := index_of(actual_o_i_state, sorted_o_i_states);
 815       /* Cardinal measures seem too easy to abuse so we convert them to an 
 816          ordinal measure. */
 817       return ix / #sorted_o_i_states;
 818     }; // end e_i_dist
 819 
 820     // Expected Utility
 821     exp_u := procedure(w, b, ti, actual_d_st, e_i, o_i_state) {
 822       /* Using our reference function, find an expression that refers to 
 823          the given output state. */
 824       o_expr_b_events := {
 825         b_event : b_event in actual_p_events(b)
 826                 | var_time(first(b_event)) == ti &&
 827                   ref(w, b)[b_event] != om &&
 828                   exists(w_state in ref(w, b)[b_event] |
 829                     exists(b_ev in lf_inv(b)[o_i_state] |
 830                       restricted_eq(w_state, assign_time(b_ev, ti+1))
 831                     )
 832                   )
 833       };
 834       assert(o_expr_b_events != {}, "No o_expr_b_events found");
 835       o_expr := lf_cm_p_inv(b, first(o_expr_b_events));
 836       // Todo: Handle multiple exprs referring to o_i_state
 837       /* Is the above too indirect and complicated? There may be worries of 
 838          not capturing the correct mode of presentation? Could we "hardcode"
 839          something into the language instead? Like with input vars or
 840          memories using At_t. Or the simplest may be to allow it to overlap
 841          with input vars. That is actually still allowed by the above. 
 842            Is this not so easy though since it needs to refer to a *future* o 
 843          state?
 844 
 845          Add up the expectations of utility. Here we are interpreting our   
 846          utility vars as additive values. U(x & y) = U(x) + U(y). If, 
 847          however, there are exceptions, they can still be encoded by 
 848          having a util var associated with the conjunction. Then, if U(x)
 849          and U(y) are still defined, you may need to be careful to encode 
 850          only the intended difference from additive in the conjunction 
 851          rather than doubly counting its full value. 
 852            Here, we are assuming the P(o []-> u) beliefs reflect the agent's
 853          judgment of overall utility. If the agent is poor at aggregating 
 854          utilities, their final judgment might come apart from these 
 855          credences. There may also be issues with the timing of these
 856          and any aggregated judgments. While this may require much 
 857          technical work to thoroughly address, we hope it is at least 
 858          conceptually and philosophical clear what is to be done. */
 859       return +/ {  actual_d_st[ p[BoxArrow(o_expr, u_expr)] ] // P(o []-> u)
 860                  * actual_d_st[e_i_j] : [u_expr, e_i_j] in e_i }; // * u
 861     }; // end exp_u
 862 
 863 // Probabilistic Coherence 
 864 // =======================
 865 
 866   incoherence := procedure(b) {
 867     /* Synchronic irrationality
 868        Avg of distances to the closest coherent probability distribution 
 869        at each time normalized by max distance. */
 870     sync_irrat := avg({ p_dist(b, ti) / max_p_dist(b, ti) : ti in [1..b.n] });
 871     /* Diachronic irrationality
 872        Probabilities either stay the same or get updated to be close to what
 873        a (locally) ideally rational inference would result in.  */
 874     dia_irrat := 1 - p_conn_continuity([ f(b)[drop_time(b.a[ti])]
 875                                          : ti in [1..b.n] ]);
 876     return avg([sync_irrat, dia_irrat]);
 877   };
 878 
 879   /* Maximum Probability Distance 
 880      Find the probability distribution that is the farthest distance from the 
 881      given brain's probability distribution and return that distance.
 882      This is used to normalize probability distance scores.  */
✔ 883   max_p_dist := procedure(b, ti) {
 884     poss_p_states := [poss_p : poss_p in possible_states(p_vars(), r)];
 885     p_states := prob_states_t(b, ti);
 886     farthest_pp := sort_list(poss_p_states, procedure(pp1,pp2) {
 887                                return prob_distance(p, cp, p_states, pp1) >
 888                                       prob_distance(p, cp, p_states, pp2);
 889                              })[1];
 890     return prob_distance(p, cp, p_states, farthest_pp);
 891   };
 892 
 893   /* Returns the set of possible causal models formed from the base variables
 894      in the domain of p. */
✔ 895   poss_cms := procedure() {
 896     base_vars := [ p[expr] : expr in domain(p) |
 897                    isString(expr) || (isTerm(expr) && fct(expr) == 'At_t') ];
 898     vs := { v : v in base_vars };
 899     orderings := permutations(base_vars);
 900     return +/ { poss_cms_from_l(l, vs) : l in orderings };
 901   };
 902 
✔ 903     poss_cms_from_l := procedure(l, vs) { // l is an ordering (list)
 904       // Each var's poss parents are sets containing the preceding vars in l.
 905       poss_v_parents := { [l[j], pow({ v : v in l[1..j-1] })] : j in [2..#l] };
 906       poss_v_parents[l[1]] := {{}};
 907       poss_parents := possible_states(vs, poss_v_parents);
 908 
 909       return +/ { poss_cms_from_p_pars(vs, poss_parents, p_pars)
 910                   : p_pars in poss_parents };
 911     };
 912 
 913     /* Given a set of parenthood relations, construct its set of possible 
 914        causal models. For each variable, construct the set of possible 
 915        functions from its parents. */
✔ 916     poss_cms_from_p_pars := procedure(vs, poss_parents, p_pars) {
 917       cm_u := { v : v in vs | p_pars[v] == {} };
 918       cm_v := vs - cm_u;
 919       cm_r := { [v, {true, false}] : v in vs };
 920       poss_v_cm_fs := {
 921         [v, function_space(possible_states(p_pars[v], cm_r), {true, false})]
 922         : v in cm_v };
 923       poss_cm_fs := possible_states(cm_v, poss_v_cm_fs);
 924       return { causal_model(cm_u, cm_v, cm_r, cm_f, om) : cm_f in poss_cm_fs };
 925     };
 926 
 927   /* Takes a causal_model and returns a set of coherent probability 
 928      distributions compatible with the cm. Each distribution is given by
 929      a pair of assignments of values to p and cp.  */
✔ 930   coh_pcms := procedure(cm) {
 931     // Coherent probability distributions for exogenous variables u
 932     coh_u_probs := { p_u : p_u in poss_p_us(cm.u)
 933                          | p_u_is_coherent(p_u, cm.u) };
 934     return { [probs(cm, p_u) + subj_conds(cm, p_u), cond_probs(cm, p_u)]
 935              : p_u in coh_u_probs };
 936   };
 937 
 938     poss_p_us := procedure(us) {
 939       return choices({ {state} >< p_range() : state in state_space(us) });
 940     };
 941 
 942       p_range := procedure() {
 943         return r[first(range(p))]; // assume all probs share the same range
 944       };
 945 
 946       /* For each prob variable, choose either it being true or false */
 947       state_space := procedure(vs) {
 948         return choices({ {[v, true], [v, false]} : v in vs });
 949       };
 950 
 951     p_u_is_coherent := procedure(p_u, base_vars) {
 952       poss_exprs := da().add_up_to(base_vars, 2 ** #base_vars);
 953       poss_probs := possible_states(poss_exprs,
 954                                     { [expr, p_range()] : expr in poss_exprs });
 955       poss_ord_pairs := poss_exprs >< poss_exprs;
 956       poss_cond_probs := possible_states(poss_ord_pairs,
 957                                 { [pair, p_range()] : pair in poss_ord_pairs });
 958       poss_p_cps := poss_probs >< poss_cond_probs;
 959       return exists(p_cp in poss_p_cps
 960                     | is_superset_of(p_cp, p_u) && superset_is_coherent(p_cp) );
 961     };
 962 
 963       is_superset_of := procedure(p_cp, p_u) {
 964         return { [p_var, p_val] : [p_var, p_val] in p_u | p_val != om }
 965                < first(p_cp);
 966       };
 967 
 968       superset_is_coherent := procedure(p_cp) {
 969         d := decision_algorithm.new();
 970         d.p := { [expr, 'P(' + str(expr) + ')']
 971                  : [expr, p_val] in first(p_cp) };
 972         d.cp := { [l, 'P(' + str(l[1]) + '|' + str(l[2]) + ')']
 973                   : [l, p_val] in last(p_cp) };
 974         pp := { ['P(' + str(expr) + ')',                   p_val]
 975                 : [expr, p_val] in first(p_cp) } +
 976               { ['P(' + str(l[1]) + '|' + str(l[2]) + ')', p_val]
 977                 : [l, p_val] in last(p_cp) };
 978         return d.is_coherent(pp);
 979       };
 980 
 981     /* Given p_u, a prob distr over states of the exogenous variables u, use 
 982        the causal_model to calculate the probabilities of endogenous vars vs. */
 983     probs := procedure(cm, p_u) {
 984       // For each state of exogenous vars u, use the causal model to fill in 
 985       // what the state of endogenous vars v would be. 
 986       p_uv := { [u_state + cm.response(cm.v, u_state), p_val]
 987                 : [u_state, p_val] in p_u };
 988       // For each poss event of the causal model, turn the event into an expr
 989       // and assign it probability equal to the sum of the probabilities of 
 990       // uv states in which the event is realized.
 991       return { [ func_to_expr(g_vs),
 992                  +/ { p_val : [uv_state, p_val] in p_uv | g_vs < uv_state }]
 993                : g_vs in cm.poss_events() };
 994     };
 995 
 996     /* Next we calculate the conditional probabilities for a given p_u */
 997     cond_probs := procedure(cm, p_u) {
 998       return +/ { calc_cond_prob(g, h) : [g,h] in cm.poss_events() ** 2 };
 999     };
1000 
1001       calc_cond_prob := procedure(cm, p_u, g, h) {
1002         if (compatible_values(g, h)) {
1003           a := func_to_expr(g);
1004           b := func_to_expr(h);
1005           c := func_to_expr(g + h);
1006           /* Using P(A|B) == P(And(A,B)) / P(B)  (Kolmogorov definition) */
1007           return { [ cp[[a,b]], probs(cm, p_u)[c] / probs(cm, p_u)[b] ] };
1008         } else {
1009           return 0;
1010         }
1011       };
1012 
1013     // Just set to 100% if the subjunctive conditional is true in cm
1014     subj_conds := procedure(cm, p_u) {
1015       return { [p[BoxArrow(func_to_expr(g), func_to_expr(h))], 1.0]
1016                 : [g,h] in cm.poss_events() ** 2
1017                 | cm.response(domain(h), g) == h };
1018     };
1019 
1020   // Note that the function it returns assigns true/false to prob vars and not
1021   // atomic expressions. You may want expr_to_events instead.
✔1022   expr_to_p_funcs := procedure(expr, dom) {
1023     return { { [p[term], bool] : [term, bool] in event }
1024              : event in expr_to_events(expr, dom) };
1025   };
1026 
1027   /* Coherent Causal Model Probabilities
1028      Coherent probability distributions over p and cp, including the 
1029      subjunctive conditionals, which can be seen as pieces of causal models. 
1030      We start with probability distributions over all causal models (from
1031      the set of base variables in p). Collecting the coherent distributions 
1032      over p and cp within each model, we then distribute the probability of
1033      the causal model to those distributions and sum them all up again. */
1034   coh_cm_ps := procedure() {
1035     // Possible probabilities of causal models
1036     poss_p_cms := choices({ {poss_cm} >< p_range : poss_cm in poss_cms() });
1037     /* The probabilities within any distribution must sum to 1. 
1038        (Each causal model considered is global and includes all base vars so 
1039        there is no worries of overlapping by one cm being a "superset" of 
1040        another.) */
1041     coh_p_cms := { p_cms : p_cms in poss_p_cms | +/ range(p_cms) == 1.0 };
1042 
1043     // Collect from each coherent probability distribution over causal models
1044     // the coherent probability distributions over p and cp that are allowed.
1045     return +/ { sum_p_cms(p_cms) : p_cms in coh_p_cms };
1046 
1047     /* Todo: Double-check whether it's necessary to expand the probability 
1048        distributions to non-canonical expressions in p? Now that prob_distance
1049        handles logical equivalences, it seems unnecessary.  */
1050   };
1051 
1052     /* Given a coherent probability distribution over causal models... */
1053     sum_p_cms := procedure(p_cms) {
1054       /* For each causal model and its probability, collect the possible
1055          choices of a coherent probability distribution from each, where
1056          those probability distributions have had the probability of the 
1057          causal model distributed over them.  */
1058       sets_of_p_cps := choices({
1059         { distr_p_cm(p_cp, p_cm) : p_cp in coh_pcms(cm) }
1060         : [cm, p_cm] in p_cms
1061       });
1062 
1063       /* ... For each choice of p_cps from each causal model, sum them up. */
1064       return { foldr(add_p_distr, {}, [p_cp : p_cp in p_cps])
1065                : p_cps in sets_of_p_cps };
1066     };
1067 
1068       /* Distribute probability of causal model.
1069          Takes p_cp, a set of pairs of coherent probability distributions over p
1070          and cp, and a probability of the causal model p_cm and then 
1071          distributes the probability of the causal model so that the probability
1072          of each expression is reduced by multiplying the p_cm. */
1073       distr_p_cm := procedure(p_cp, p_cm) {
1074         // p_cp == [cm_p, cm_cp]
1075         cm_p := p_cp[1];
1076         cm_cp := p_cp[2];
1077         return [{ [p_var, p_val * p_cm] : [p_var, p_val] in cm_p },
1078                 { [cp_l, cp_val * p_cm] : [cp_l, cp_val] in cm_cp }];
1079       };
1080 
1081       /* Given two pairs of probability distributions over p_vars
1082          add up the probabilities of expressions. */
✔1083       add_p_distr := procedure(p_cp1, p_cp2) {
1084         p1  := p_cp1[1];
1085         cp1 := p_cp1[2];
1086         p2  := p_cp2[1];
1087         cp2 := p_cp2[2];
1088         return [sum_p(p1, p2), sum_p(cp1, cp2)];
1089       };
1090 
✔1091         sum_p := procedure(p1, p2) {
1092           /* If one has a variable where the other does not have any variable
1093              with an equivalent expression, just go with the probability 
1094              defined by the one. */
1095           return { [v1, p1[v1]] : v1 in domain(p1)
1096                    | !exists(v2 in domain(p2) | equiv_p_expr(p, cp, v1, v2)) } +
1097                  { [v2, p2[v2]] : v2 in domain(p2)
1098                    | !exists(v1 in domain(p1) | equiv_p_expr(p, cp, v1, v2)) } +
1099           /* Otherwise, for any variables that have equivalent expressions,
1100              add up the probabilities for those variables. (Since they've 
1101              already been reduced in distr_p_cm, we don't need to average 
1102              the sum.)  */
1103                  +/ { { [v1, p1[v1] + p2[v2]],[v2, p1[v1] + p2[v2]]  }
1104                       : [v1, v2] in domain(p1) >< domain(p2)
1105                       | equiv_p_expr(p, cp, v1, v2) };
1106         };
1107 
1108           equiv_p_expr := procedure(p, cp, v1, v2) {
1109             e1 := p_cp_inv(p, cp, v1);
1110             e2 := p_cp_inv(p, cp, v2);
1111             return equiv_expr(e1, e2, all_atomic_formulas(domain(p)));
1112           };
1113 
1114   /* Takes a brain and time and finds the closest perfectly coherent 
1115      probability distribution and returns the distance to it. */
1116   p_dist := procedure(b, ti) {
1117     p_states := prob_states_t(b, ti);
1118     return prob_distance(p, cp, sorted_rat(p_states)[1], p_states);
1119   };
1120 
1121   /* Takes a prob state and returns a list of coherent probability 
1122      distributions sorted by how close they are to p_states, closer ones first.
1123   */
1124   sorted_rat := procedure(p_states) {
1125     return sort_list( [ coh_p + coh_cp : [coh_p, coh_cp] in coh_cm_ps() ],
1126       /* A procedure measuring which of two probability states is closer to 
1127          the original one given.  */
1128       procedure(pp1, pp2) {
1129         return prob_distance(p, cp, pp1, p_states) <
1130                prob_distance(p, cp, pp2, p_states);
1131       }
1132     );
1133   };
1134 
1135   /* Takes a p or cp var in range(p) + range(cp) and returns its preimage 
1136      formula(s) */
✔1137   p_inv := procedure(v) {
1138     if (v in range(p)) {
1139       return inv(p)[v];
1140     } else {
1141       return inv(cp)[v];
1142     }
1143   };
1144 
1145   // Same as p_inv but with p and cp explicitly passed in due to setlx bug
1146   p_cp_inv := procedure(p, cp, v) {
1147     if (v in range(p)) {
1148       return inv(p)[v];
1149     } else {
1150       return inv(cp)[v];
1151     }
1152   };
1153 
1154   // Same as p_inv but if in cp, it returns the first expr instead of the pair
1155   p_var_inv := procedure(v) {
1156     if (v in range(p)) {
1157       return inv(p)[v];
1158     } else {
1159       return first(inv(cp)[v]);
1160     }
1161   };
1162 
1163 
1164   /* Obeys the axioms of probability.
1165        See especially p 45 (or 64 in pdf) of E.T. Jaynes, Probability Theory: 
1166        The Logic of Science. https://bayes.wustl.edu/etj/prob/book.pdf  */
1167   old_is_coherent := procedure(pp) {
1168     /* For easier handling, turn domain(p) into a datatype like domain(cp) 
1169        so that e.g. P(A) looks more like P(A|om) */
✔1170     force_list := procedure(v) {
1171       if (isList(p_inv(v))) {
1172         return p_inv(v);
1173       } else {
1174         return [p_inv(v), om];
1175       }
1176     };
1177     pp := { [force_list(v), num] : [v,num] in pp };
1178     obeys_axiom_3 := procedure(l) {
1179       if (isTerm(l[1]) && fct(l[1]) == "And") { // [And(a,b), c]
1180         [a,b] := args(l[1]);
1181         c := l[2];
1182         // P(a,b|c) = P(a|b,c) * P(b|c)
1183         return pp[l] == pp[ [a, And(b,c)] ] * pp[ [b,c] ];
1184       } else {
1185         return true;
1186       }
1187     };
1188     return forall(l in domain(pp) | pp[l] >= 0) &&
1189            // P(A|x) + P(~A|x) = 1
1190            // Todo: Simplify double negation to avoid infinite NOT() regression?
1191            forall(l in domain(pp) | pp[l] == 1 - pp[ [Not(l[1]), l[2]] ]) &&
1192            forall(l in domain(pp) | obeys_axiom_3(l));
1193   }; // end old_is_coherent
1194 
1195   /* From Lasky, Kathryn. "Axiomatic First-Order Probability" 
1196      http://ceur-ws.org/Vol-527/paper5.pdf 
1197 
1198       Laskey axioms
1199         P1. probabilities are between 0 and 1
1200         P2. probabilities in tautologies are 1
1201               or just logical truths
1202         P3. if probability in two statements both being true are 0, then 
1203               probability of one or the other is equal to adding probability 
1204               in each
1205         P4. Bayesian conditioning
1206         P5. interchangeability of logically equivalent statements
1207 
1208      Todo: Double-check if it's necessary to handle undefined/om probability 
1209            values. It seems p_u_is_coherent checks its coherence by seeing if
1210            a superset is perfectly coherent so I think that strategy should 
1211            work. But there may be some slight technical issues making sure 
1212            we're allowing or disallowing om in the right places there.
1213   */
1214   is_coherent := procedure(pp) {
1215     pp := { [force_list(v), num] : [v,num] in pp };
1216     return forall(l in domain(pp) |
1217       // P1: Probabilities are between 0 and 1.
1218       0 <= pp[l] && pp[l] <= 1 &&
1219       // P2: Logical truths have probability 1.
1220       (!is_logical_truth(l[1]) || pp[l] == 1) &&
1221       forall(l2 in domain(pp) |
1222         ( l[2] != l2[2] || (
1223           // z is shared in P(_|z) && P(_|z)
1224 
1225           // P3: If P(x^y|z) = 0, then P(x v y|z) = P(x|z) + P(y|z)
1226           ( pp[[And(l[1], l2[1]), l[2]]] != 0 ||
1227             pp[[ Or(l[1], l2[1]), l[2]]] == pp[l] + pp[l2] ) &&
1228 
1229           // P4: Bayesian conditioning. P(x^y|z) = P(y|z) * P(x|y,z)  
1230           ( fct(l[1]) != "And" || !(l2[1] in args(l[1])) ||
1231             forall(l3 in domain(p) |
1232               !(l3[1] in args(l[1])) || l3[1] == l2[1] ||
1233               l3[2] != And(l2[1], l[2]) || pp[l] == pp[l2] * pp[l3]
1234             ) ) &&
1235 
1236           // P5: Interchangeability of equivalent expressions. Part 1
1237           //     If x<->y, then Vz P(x|z) = P(y|z) 
1238           ( !equiv_expr(l[1], l2[1], atomic_formulas(domain(p))) ||
1239             pp[l] == pp[l2] )
1240         ) ) /* end || */ && (
1241           // P5 Part 2: If x <-> y, then Vz P(z|x) = P(z|y) 
1242           !equiv_expr(l[2], l2[2], atomic_formulas(domain(p))) ||
1243           l[1] != l2[1] || pp[l] == pp[l2]
1244         )
1245       ) // end forall l2
1246     ); // end forall l
1247   }; // end is_coherent
1248 
1249     /* For easier handling, turn domain(p) into a datatype like domain(cp) 
1250        so that e.g. P(A) looks more like P(A|om) */
✔1251     force_list := procedure(v) {
1252       if (isList(p_inv(v))) {
1253         return p_inv(v);
1254       } else {
1255         return [p_inv(v), om];
1256       }
1257     };
1258 
1259   /* Takes two functions mapping p & cp vars to probabilities and computes
1260      the difference. See Staffel, Julia. Measuring the Overall Incoherence of 
1261      Credence Functions. Synthese, 2015. DOI 10.1007/s11229-014-0640-x 
1262 
1263      Technical Note: Takes p and cp (which should just be the usual this.p and 
1264      this.cp) but needs to be passed explicitly because of a setlx bug: The 
1265      second and subsequent calls to an instance procedure within a nested 
1266      procedure is not able to access instance variables / procedures. 
1267 
1268      See ambitiousness for a more general workaround. There and elsewhere we
1269      assign *this* (the decision algorithm instance) to *self* and then pass
1270      in self as the first parameter. The receiving instance procedure then
1271      makes sure to call any instance variables and procedures on self rather 
1272      than their implicit and buggy this. The result may be likened to Python's
1273      way of handling instance methods.
1274   */
✔1275   prob_distance := procedure(p, cp, pp1, pp2) {
1276     /* First pass: (but doesn't handle undefineds and logical equivalents)
1277     return +/ { abs(pp1[v] - pp2[v]) : v in domain(pp1) | v in domain(pp2) };
1278     // Second pass: (but doesn't handle double-counting)
1279     return +/ { abs(pp1[v] - pp2[v2]) : [v, v2] in domain(pp1) >< domain(pp2)
1280                                       | v == v2 || equiv_p_expr(v, v2) };     
1281        Consider three people where the "true" probability is 90%
1282          Person 1: A & B 80%, B & A 70%
1283          Person 2: A & B 80%
1284          Person 3: A & B 80%, B & A 80%
1285        Averaging probabilities in logical equivalents favors person 2 and 3 
1286        over 1 but not 2 over 3.
1287     */
1288     return +/ { abs( pp_equiv(p, cp, pp1)[p_class] -
1289                      pp_equiv(p, cp, pp2)[p_class] )
1290                 : p_class in p_equiv_classes(p, cp)
1291                 | pp_equiv(p, cp, pp1)[p_class] != om &&
1292                   pp_equiv(p, cp, pp2)[p_class] != om };
1293   };
1294 
1295     // Equivalence classes of probability variables based on logical equivalence
1296     p_equiv_classes := procedure(p, cp) {
1297       return { { x : x in range(p) + range(cp)
1298                    | equiv_p_expr(p, cp, p_var, x) }
1299                : p_var in range(p) + range(cp) };
1300     };
1301 
1302     // Converts a possibility probability distribution pp to one that ranges
1303     // over equivalence classes of logically equivalent p vars instead of 
1304     // directly over the p vars.
1305     pp_equiv := procedure(p, cp, pp) {
1306       return { [p_class, avg_p_class(pp, p_class)]
1307                : p_class in p_equiv_classes(p, cp)
1308                | avg_p_class(pp, p_class) != om };
1309     };
1310 
1311       // Return the average of the values pp assigns to the p vars in p_subset
1312       avg_p_class := procedure(pp, p_subset) {
1313         p_vals := [ pp[p_var] : p_var in domain(pp) | p_var in p_subset ];
1314         if (#p_vals == 0) {
1315           return om;
1316         } else {
1317           return avg(p_vals);
1318         }
1319       };
1320 
1321 // Helpers 
1322 // -------
1323 
✔1324   poss_io_states := cachedProcedure() {
1325     return possible_states(i + o, r);
1326   };
1327 
✔1328   poss_s_states := cachedProcedure() {
1329     return possible_states(s(), r);
1330   };
1331 
✔1332   poss_m_states := cachedProcedure() {
1333     return possible_states(m, r);
1334   };
1335 
1336   poss_m2_states := cachedProcedure() {
1337     return possible_states(m2, r);
1338   };
1339 
1340   poss_ms_states := cachedProcedure() {
1341     return possible_states(m + m2, r);
1342   };
1343 
✔1344   poss_i_states := cachedProcedure() {
1345     return possible_states(i, r);
1346   };
1347 
✔1348   poss_is_states := cachedProcedure() {
1349     return possible_states(i + s(), r);
1350   };
1351 
✔1352   poss_o_states := cachedProcedure() {
1353     return possible_states(o, r);
1354   };
1355 
✔1356   poss_u_states := cachedProcedure() {
1357     return possible_states(range(u), r);
1358   };
1359 
1360 
1361 // Best Compression
1362 // ================
1363 
1364   /* Complexity of Intentional Explanation
1365      -------------------------------------
1366      This can be seen as a more realist and more formal version of Dennett's
1367      Intentional Stance. 
1368        See e.g. https://sites.google.com/site/minddict/intentional-stance-the
1369 
1370      On a first pass, the best intentional explanation can be taken to be the
1371      one which best compresses the brain's behavior.
1372        See better_explanation for further considerations.
1373 
1374      Also see https://en.wikipedia.org/wiki/Minimum_description_length:
1375        "The minimum description length (MDL) principle is a formalization of 
1376         Occam's razor in which the best hypothesis (a model and its parameters) 
1377         for a given set of data is the one that leads to the best compression 
1378         of the data." 
1379 
1380      Since b and d already contain information on their transitions from any 
1381      possible state, we don't need to run this for each time step.
1382   */
1383   complexity := cachedProcedure(b) {
1384     // Complexity of b given d and f + Complexity of d and f
1385     raw_score := k_given(b.t_to_str(), df_to_str(b)) + k(df_to_str(b));
1386     /* Now normalize. Worst case is it doesn't help encode b any better and 
1387        it's just as complex as b. Best case is if it could take 0 bits.  */
1388     worst_score := 2 * k(b.t_to_str());
1389     return 1 - raw_score / worst_score;
1390   };
1391 
1392   to_s := cachedProcedure() {
1393     return str([i, p, cp, u, m, m2, n, o, r, t()]);
1394   };
1395 
1396   f_to_s := procedure(b) {
1397     return str(f(b));
1398   };
1399 
1400   df_to_str := procedure(b) {
1401     return to_s() + "@" + f_to_s(b);
1402     // '@' is just a separator, an otherwise unused character
1403   };
1404 
1405   /* Ambitiousness
1406      -------------
1407      If we only optimized for the best compression of the brain, we face the 
1408      following problem. Suppose the syntax we use is somewhat inefficient. 
1409      Then, the smallest K(b|df) + K(df) might be produced by an empty d with 
1410      all the work being done by a turing machine which generates b using 
1411      essentially the same decision algorithm we would have wanted to use as d 
1412      but with a more efficient syntax. Or it may only put some into the 
1413      official d and sneak in the rest in the turing machine. It seems what
1414      we'd need is something like a not-a-decision-algorithmic-explanation
1415      predicate to apply to the turing machine. Or we want d to be ambitious, 
1416      ideally packing as much of a decision-algorithmic explanation as possible
1417      or at least positively weighing its ambitiousness against potential 
1418      increases in complexity.
1419      
1420      For a given d, we consider the auxiliary hypothesis h, which together w/
1421      d best explains b. We then look for a decomposition of h into [h_i, h_j] 
1422      where [h_i, h_j] is similar to h, and [h_i, h_j] makes d least ambitious, 
1423      meaning that the d* which is a superset of d and maximizes coherence and 
1424      similarity to d + h_i, improves coherence the least with the greatest 
1425      complexity cost. d's ambitiousness in the worst case decomposition is d's 
1426      ambitiousness. In other words, the more there is a d* which is highly 
1427      similar to d + some h_i and very coherent, the less ambitious d is. It 
1428      would leave out too much that could and should be explained using a 
1429      decision algorithmic explanation. If d is very ambitious, there's more 
1430      like just noise left for the auxiliary hypothesis or you'd have to stray 
1431      farther from the auxiliary hypothesis h to subsume it under a decision 
1432      algorithmic explanation.
1433   */
1434   ambitiousness := procedure(b) {
1435     poss_hs := all_strs_lte(#b.t_to_str()) >< all_strs_lte(#b.t_to_str());
1436     self := this; // workaround for setlx bug described in prob_distance
1437     poss_hs := sort_set(poss_hs,
1438       /* Procedure for worse decomposition. Calling it worse rather than
1439          better because we want the [h1, h2] which represents the worst case
1440          scenario as far as ambitiousness goes.  
1441       */
1442       procedure(hs_i, hs_j) {
1443         return hs_score(self, b, hs_i) > hs_score(self, b, hs_j);
1444       });
1445     hs := poss_hs[1];
1446     return ambitiousness_with_hs(b, hs);
1447   };
1448 
1449     hs_score := procedure(self, b, hs_k) {
1450       return self.hs_similarity(b, hs_k) - self.ambitiousness_with_hs(b, hs_k);
1451     };
1452 
1453     hs_similarity := procedure(b, hs_k) { // hs_k == [h1, h2]
1454       return ( k_given(h(b), str(hs_k)) + k_given(str(hs_k), h(b)) ) * -1;
1455       // or ** -1 ?
1456     };
1457 
1458   // Stringified auxiliary hypothesis which together with d explains b.t_to_str
1459   h := procedure(b) {
1460     poss_hs := all_strs_lte(#b.t_to_str());
1461     self := this; // workaround for setlx bug described in prob_distance
1462     poss_hs := sort_set(poss_hs, procedure(h_i, h_j) { // better h explanation
1463                  return h_complexity(self, b, h_i) < h_complexity(self, b, h_j);
1464                });
1465     return poss_hs[1];
1466   };
1467 
1468     h_complexity := procedure(self, b, h_k) {
1469       return k_given(b.t_to_str(), self.df_to_str(b) + "|" + h_k);
1470     };
1471 
1472   ambitiousness_with_hs := procedure(b, hs_k) {
1473     poss_d_stars := { poss_d_star : poss_d_star in supersets_lte(b)
1474                       | poss_d_star.is_valid() &&
1475                         poss_d_star.is_implemented_by(b) };
1476     self := this; // workaround for setlx bug described in prob_distance
1477     poss_d_stars := sort_set(poss_d_stars,
1478       procedure(d_star_i, d_star_j) { // better_d_star
1479         return d_star_sim(self, b, hs_k, d_star_i) - d_star_i.incoherence(b) >
1480                d_star_sim(self, b, hs_k, d_star_j) - d_star_j.incoherence(b);
1481       });
1482     d_star := poss_d_stars[1];
1483 
1484     delta_incoh := ( d_star.incoherence(b) - incoherence(b) ) / incoherence(b);
1485     delta_irrat := ( d_star.instr_irrat(b) - instr_irrat(b) ) / instr_irrat(b);
1486     delta_compl := (k(d_star.df_to_str(b)) - k(df_to_str(b))) / k(df_to_str(b));
1487     /* More incoherent and irrational -> more ambitious
1488          because it's like less of real Decision Algorithmic stuff left in h1
1489        Larger complexity -> less ambitious 
1490          because there's more Decision Algorithmic stuff left in hs_1 & not in d
1491          but maybe replace complexity with more like raw size? #states?  */
1492     return delta_incoh + delta_irrat - delta_compl;
1493   };
1494 
1495     d_star_sim := procedure(self, b, hs_k, d_star_k) {
1496       raw_sim := (  // roughly, K(d*|d,h1) + K(d,h1|d*_s)
1497         k_given( d_star_k.df_to_str(b), self.df_to_str(b) + "|" + hs_k[1]) +
1498         k_given( self.df_to_str(b) + "|" + hs_k[1],
1499                  d_star_k.simplest_version(b).df_to_str(b) )
1500       );
1501       /* Normalize. Best similarity is if 0 extra bits are required. 
1502          Worst is K(d*) + K(d); the given bits didn't help at all. */
1503       worst_sim := k(d_star_k.df_to_str(b)) + k(self.df_to_str(b));
1504       return 1 - raw_sim / worst_sim;
1505     };
1506 
1507   /* Returns decision algorithms with # of possible states <= #b.poss_states
1508      which are "supersets" of self. It has additional variables and therefore
1509      states, but when considering just the variables shared with self, it is 
1510      isomorphic to self.  */
1511   supersets_lte := procedure(b) {
1512     return { d : d in decision_algorithm.all_lte(#b.poss_states())
1513                | is_subset_of(d) };
1514   };
1515 
1516   // Returns whether this decision algorithm is a "subset" of the given d
1517   is_subset_of := procedure(d) {
1518     // i, o, p, cp, u, m, m2, n, r, t_s, t_o
1519     var_pairs := { [i, d.i], [o, d.o], [p, d.p], [cp, d.cp],
1520                    [u, d.u], [m, d.m], [m2, d.m2] };
1521     vars_are_subsets := forall([vs, d_vs] in var_pairs | vs < d_vs);
1522     if (!vars_are_subsets || #n > #d.n) { return false; }
1523 
1524     n_are_subsets := forall(j in [1..#n] |
1525                        forall(ltr in {'e','m2','o'} |
1526                          n[j][ltr] < d.n[j][ltr] ));
1527     if (!n_are_subsets) { return false; }
1528 
1529     /* For all transitions from a i+s state to a s+o state in self, it is the
1530        case that any transition in d starting from a superset of i+s ends in
1531        a d state that is a superset of the s+o state.  */
1532     return forall([is, so] in t() |
1533              forall(ccs in compatible_complete_states(is, d.poss_is_states()) |
1534                compat(so, d.t()[ccs])
1535              )
1536            );
1537   };
1538 
1539   is_simplest_version := procedure(b) {
1540     return is_equal_to(simplest_version(b));
1541   };
1542 
1543   /* Using simplest_version handles worries with using m as arbitrary data
1544      to smuggle in unlabelled decision algorithmic information. Only the 
1545      decision algorithmic aspects of a decision algorithm should do the 
1546      explaining. This should also handle worries of higher-order utility
1547      information being smuggled in within the memory variables.  */
1548   simplest_version := procedure(b) {
1549     alt_ds := [ d : d in decision_algorithm.all(b)
1550                   | is_isomorphic_to(d) && d.is_implemented_by(b) ];
1551     alt_ds := sort_list(alt_ds, decision_algorithm.simpler);
1552     return alt_ds[1];
1553   };
1554 
✔1555   is_equal_to := procedure(d) {
1556     l1 := [  i,   o,   p,   cp,   u,   m,   m2,   n,   r,   t_s,   t_o];
1557     l2 := [d.i, d.o, d.p, d.cp, d.u, d.m, d.m2, d.n, d.r, d.t_s, d.t_o];
1558     return l1 == l2;
1559   };
1560 
1561   is_isomorphic_to := procedure(d) {
1562     /* Everything but the memory variables is the same 
1563        And there is an isomorphism between m+m2 states and d.m+d.m2 states
1564        Todo: Also add n minus m2s in n to simple equality comparison.
1565     */
1566     l1 := [  i,   o,   x,   p,   cp,   u,   r,   t_s,   t_o];
1567     l2 := [d.i, d.o, d.x, d.p, d.cp, d.u, d.r, d.t_s, d.t_o];
1568     return l1 == l2 && exists(fm in possible_fms(d) | fm_commutes(fm, d));
1569   };
1570 
1571     // Todo: Also do higher-order m2s
✔1572     possible_fms := procedure(d) {
1573       /* Construct the space of functions from states of m+m2 to d.m+d.m2,
1574          respecting the m / m2 boundary */
1575       fm_ms  := {
1576         { [ m_st + m2_st,  fm_m[m_st] + fm_m2[m2_st] ]
1577           : [m_st, m2_st] in poss_m_states() >< poss_m2_states() }
1578         : [fm_m, fm_m2] in
1579           function_space(possible_states(m,  r), possible_states(d.m,  d.r)) ><
1580           function_space(possible_states(m2, r), possible_states(d.m2, d.r))
1581       };
1582 
1583       // For convenience map everything else onto its counterpart in d
1584       fms := {
1585         { [iso, apply_fm_m(fm_m, iso) ] : iso in possible_states(i+s()+o, r) }
1586         : fm_m in fm_ms
1587       };
1588       return fms;
1589     };
1590 
1591       // Todo: Also do higher-order m2s.
✔1592       apply_fm_m := procedure(fm_m, iso) {
1593         iso_m := { [var, val] : [var, val] in iso | var in m || var in m2 };
1594         return { [v, iso[v]] : v in i + s() + o - m - m2 } + fm_m[iso_m];
1595       };
1596 
✔1597     fm_commutes := procedure(fm, d) {
1598       // Restrict fm to just i + s() variables
1599       fm_is := { [{ [var, val] : [var, val] in iso1 | var in i + s() },
1600                   { [var, val] : [var, val] in iso2 | var in d.i + d.s() }]
1601                     : [iso1, iso2] in fm };
1602       // Restrict fm to just s() + o variables
1603       fm_so := { [{ [var, val] : [var, val] in iso1 | var in s() + o },
1604                   { [var, val] : [var, val] in iso2 | var in d.s() + d.o }]
1605                     : [iso1, iso2] in fm };
1606       return { fm_so[ t()[g_is] ] == t()[ fm_is[g_is] ] : [g_is, h_so] in t()
1607              } == { true };
1608     };
1609 
1610 // Rationality
1611 // ===========
1612 
1613   /* Rational Utility Function
1614      -------------------------
1615      Takes the world w and brain b and collects all possible continuations of
1616      brain/decision states using bs_msr_paths. Then it weights them by 
1617      agential_identity, optimal_rxs, and subjective likelihood and finds the 
1618      center-of-mass / social-choice of the resulting first order utility 
1619      functions. 
1620 
1621      This comes out of the metaethical view developed by Howard Nye and June
1622      Ku and written up at http://www.metaethical.ai/norm_descriptivism.pdf. 
1623      There we focused on the simple case in which the norms we accept or our
1624      higher-order preferences formed a hierarchy with a single fundamental norm 
1625      or highest-order utility function governing our lower-order norms /
1626      functions. (Also see the comments above n := n towards the top.) In that 
1627      case, what we have most reason to do would be what that highest order 
1628      utility function would prescribe, perhaps through the prescription of 
1629      certain lower-level utilty functions.
1630 
1631      Elsewhere, we have acknowledged that things might be more complicated. We 
1632      might have a network of accepted norms / higher-order preferences in which 
1633      they all influence one another rather than a strict top-down hierarchy.
1634      We have suggested that in that case, the weights of each accepted norm and
1635      the parameters governing the network behavior could be treated as the 
1636      fundamental norm. Developing this further, we might model it as a markov 
1637      model with states of norm acceptances influencing other acceptances and 
1638      look for a stationary distribution, i.e. an equilibrium state in which the 
1639      state it transitions to is the same state it started with. 
1640 
1641      However, even that makes a simplifying assumption that the network 
1642      topology of which norms influence which others remains constant. But if 
1643      we imagine a brain's behavior in response to varying inputs, it seems
1644      likely that sometimes, which higher-order preferences influence which 
1645      others would also vary. To handle this, we implement a parliamentary model
1646      to aggregate the various influences across different possible 
1647      continuations of the agent. 
1648        This is inspired by Nick Bostrom and Toby Ord on Parliamentary Models 
1649      for Moral Uncertainty. Although it's applied in a different context, it's
1650      similar in that both are aggregating many utility functions into one.
1651      http://www.overcomingbias.com/2009/01/moral-uncertainty-towards-a-solution.html
1652 
1653      In the end, this does bring us closer to the ideal response / advisor
1654      family of metaethical theories but I think our focus on the influence of
1655      optimal normative judgments remains distinctive and arguably avoids some
1656      worries. We are reading off the first-order utility function from ideal
1657      selves rather than the actions so we have less distortion from the 
1658      idealization process to worry about since there's less to change. We
1659      address remaining worries about distortion with agential identity to 
1660      measure how much one remains the same agent. 
1661 
1662      The idealization is mostly done by weighting more heavily selves who are
1663      the result of normative judgments that best satisfy the decision criteria
1664      governing them. We also incorporate subjective likelihood of the inputs
1665      determining possible continuations to factor in normal operating 
1666      conditions without letting in external factors and violating supervenience
1667      on just the brain.
1668   */
1669   ruf := procedure(w, b) {
1670     t_z := 10 ** 9; // Number of time steps of continuations to consider
1671     /* Todo: Find a more principled way
1672          * "Ask" each branch how much longer to continue?
1673          * Compute infinitely but in a way that asymptotes? 
1674          * Keep computing until it converges, with minimum time? 
1675              If it never converges? */
1676 
1677     // Poss social choice utility functions
1678     psc_u_dom := domain(p) + domain(u);
1679     psc_u_rng := r[first(range(u))] + { om };
1680     psc_us := choices({ { [expr, r_i] : r_i in psc_u_rng }
1681                         : expr in psc_u_dom });
1682     psc_us := { { [expr, r_i] : [expr, r_i] in psc_u | r_i != om }
1683                 : psc_u in psc_us }; // filter out om
1684     state_space := exprs_to_state_space(psc_u_dom);
1685 
1686     voter_wts := {};
1687     t_i := 1;
1688     bs1 := drop_time(b.a[b.n]);
1689     while (t_i <= t_z) {
1690       bmps := bs_msr_paths(w, b, bs1, t_i);
1691       voter_wts := voter_wts + {
1692         [ // voter util func
1693           additive_to_ordinal( f(b)[first(last(bmp))], 0, state_space),
1694           time_wt(t_i) * voter_weight(w, b, bmp) ] // voter weight
1695         : bmp in last(bmps)
1696       };
1697       t_i := t_i + 1;
1698     }
1699     return sort_set(psc_us,
1700                     procedure(psc_u1, psc_u2) {
1701                       return rat_psc_dist(voter_wts, psc_u1, state_space) <
1702                              rat_psc_dist(voter_wts, psc_u2, state_space);
1703                     })[1];
1704   };
1705 
1706     time_wt := procedure(t_i) { return 1; }; // Placeholder constant function
1707 
1708     voter_weight := procedure(w, b, bmp) {
1709       msr := last(last(bmp));
1710       bss := [ bs : [bs, msr] in bmp ]; // Brain StateS
1711 
1712       cached_ref := om;
1713       wb := new_wb(w, b, bss);
1714       w2 := first(wb);
1715       b2 := last(wb);
1716 
1717       dss := [ f(b2)[bs] : bs in bss ];
1718       agential_id := agential_identity(dss, w2, b2);
1719       return msr * agential_id * optimal_rxs(w2, b2, dss);
1720     };
1721 
1722     // Possible Social Choice for Rationality (as opposed to in optimal_rxs)
1723     rat_psc_dist := procedure(voter_wts, psc_u, state_space) {
1724       card_u := add_u_to_card_u(psc_u, state_space);
1725       ord_u := card_u_to_ord_u( card_u, domain(card_u), r[first(p)] );
1726       return +/ { voter_wts[voter] * ord_u_dist(voter, ord_u) ** 2
1727                   : voter in domain(voter_wts) };
1728     };
1729 
1730   new_wb := procedure(w, b, bss) {
1731     b2   := b;
1732     b2.a := b2.a + [assign_time(bss[t_j], b.n + t_j) : t_j in [1..#bss]];
1733     b2.n := #(b2.a);
1734 
1735     w2   := w;
1736     w2.a := w2.a + [assign_time(bss[t_j], b.n + t_j) : t_j in [1..#bss]];
1737     w2.n := #(w2.a);
1738 
1739     return [w, b];
1740   };
1741 
1742   /* Optimal Normative Judgments / Prescriptions
1743      -------------------------------------------
1744      Returns a score for how much the list of decision states has had outputs
1745      of higher-order utility functions (i.e. normative judgments / 
1746      prescriptions) that maximized higher-order utility. If the state space
1747      of prescriptions (n[j]['o']) overlap, we favor those states voted for by 
1748      more accepted norms through a synchronic social choice function.
1749   */
1750   optimal_rxs := procedure(w, b, dss) {
1751     opts := [ optimality(w, b, dss[j], dss[j+1], b.n - (#dss - j) )
1752               : j in [1..(#dss - 1)] ];
1753     return 0.5 * min(opts) + 0.5 * avg(opts);
1754   };
1755 
1756     ue_state_space := procedure() {
1757       base_exprs := +/ { ue_base_exprs(j) : j in [1..#n] };
1758       return choices({ { [subform, true], [subform, false] }
1759                        : subform in base_exprs });
1760     };
1761 
1762     optimality := procedure(w, b, ds, ds2, t_i) {
1763       /* Social choice to balance multiple synchronic utility functions if
1764          they conflict.  */
1765       ord_us := { additive_to_ordinal(ds, j, ue_state_space()) : j in [1..#n] };
1766       sync_psc_us := choices({ { [state, r_i] : r_i in r[first(range(u))] }
1767                                : state in ue_state_space() });
1768       sc_u := sort_set(psc_us,
1769                        procedure(psc_u1, psc_u2) {
1770                          return sync_psc_dist(ord_us, psc_u1) <
1771                                 sync_psc_dist(ord_us, psc_u2);
1772                        })[1];
1773 
1774       n_o_vars := +/ { n_i['o'] : n_i in n }; // Prescription vars
1775       // Observed state of those vars in ds2
1776       obs_rxs := { [n_o_var, ds2[n_o_var]] : n_o_var in n_o_vars };
1777 
1778       // Collect all possible prescriptions along with their (higher) utilities.
1779       util_rxs := {
1780         [rxs, util_of_rxs(w, b, t_i, ds, ds2, psc_base_exprs, sc_u, rxs)]
1781         : rxs in poss_rx_states()
1782       };
1783       // Sort them by optimality.
1784       util_rxs := sort_set(util_rxs, procedure(rxs_u1, rxs_u2) {
1785                                        return last(rxs_u1) > last(rxs_u2);
1786                                      });
1787       // Return a normalized score for the obs_rxs by their percentile rank.
1788       return 1 - index_of(
1789         [ obs_rxs,
1790           util_of_rxs(w, b, t_i, ds, ds2, psc_base_exprs, sc_u, obs_rxs) ],
1791         util_rxs
1792       ) / #util_rxs;
1793     }; // end optimality
1794 
1795       sync_psc_dist := procedure(ord_us, sync_psc_u) {
1796         ord_psc_u := card_u_to_ord_u(sync_psc_u, domain(sync_psc_u),
1797                                                  r[first(p)] );
1798         return +/ { ord_u_dist(ord_u, ord_psc_u) ** 2 : ord_u in ord_us };
1799       };
1800 
1801       util_of_rxs := procedure(w, b, t_i, ds, ds2, psc_base_exprs, sc_u, rxs) {
1802         /* For the sake of simplicity, we assume that higher-order utilities 
1803            depend on only intrinsic properties of brains / decision algorithms.
1804            This means that being given the future brain states bss is 
1805            sufficient to tell us the utility of various prescriptions under 
1806            this assumed future. This assumption can be quite plausible for 
1807            higher-order utilities that enforce consistency, coherence or some
1808            form of reflective equilibrium. If we abandon this assumption, we
1809            may need to model a set of possible worlds and a probability 
1810            distribution or measure over them.
1811 
1812            We might typically expect higher-order utilities to be placed in 
1813            some change in lower-order utility and then a recognition that some
1814            prescription would more-or-less immediately cause that change would 
1815            cause the prescription and in turn, the intended change. But since
1816            we can neither assume that the higher-order utility is placed in 
1817            a specific, concrete lower-order utility change in the near future as
1818            opposed to more open-ended properties nor assume the immediacy of the
1819            prescription's causation of a lower-order utility change, we just 
1820            look very far into the future and sum up the utility of any events 
1821            in that 4-dimensional space-time block that would be included in the
1822            reference of higher-order utility expressions. Since the network
1823            topology of the higher-order utility functions may be path dependent,
1824            we also use the bs_msr_paths to aggregate over the different futures
1825            made possible by various input states weighted by their subjective
1826            likelihood.
1827         */
1828         new_ds2 := rxs + { [var, val] : [var, val] in ds2
1829                                       | !(var in domain(rxs)) };
1830         bs := inv(f(b))[new_ds2];
1831         bmps := bs_msr_paths(w, b, bs, 10 ** 9);
1832         future_wts := {                      // collect a ... 
1833           [ [first(bs_msr) : bs_msr in bmp], // list of brain states, bss,
1834             last(last(bmp)) ]                // & measure from the final state
1835           : bmp in last(bmps)                // for each bs_msr_path
1836         }; // to get { [bss, msr], ... }
1837 
1838         return +/ {
1839           msr * util_of_future(w, b, t_i, ds, psc_base_exprs, sc_u, bss)
1840           : [bss, msr] in future_wts
1841         };
1842       }; // end util_of_rxs
1843 
1844         util_of_future := procedure(w, b, t_i, ds, psc_base_exprs, sc_u, bss) {
1845           wb := new_wb(w, b, bss);
1846           w2 := first(wb);
1847           b2 := last(wb);
1848 
1849           future_state := { [expr, eval_expr(w2, b2, t_i, ds, bss, expr)]
1850                             : expr in psc_base_exprs };
1851           return sc_u[future_state];
1852         };
1853 
1854         // Returns a boolean for whether the expr is true in that future
1855         eval_expr := procedure(w, b, t_i, ds, bss, expr) {
1856           p_var := p[expr];
1857           p_event := { [p_var, ds[p_var]] };
1858           b_event := first( lf_inv_at(b,t_i)[p_event] );
1859           ref_b_event := ref(w,b)[b_event];
1860           disjuncts := { restricted_eq(w.actual_state(), disjunct)
1861                          : disjunct in ref_b_event };
1862           return #{ disj : disj in disjuncts | disj == true } > 0;
1863         };
1864 
1865   /* Extensional rational utility */
1866   ext_ruf := procedure(w, b) {
1867     uf := ruf(w,b);
1868     // Map expressions to their referents.
1869     expr_ref := { [expr, ref_expr(w, b, b.n, expr)] : [expr, r_i] in uf };
1870     // Map every possible world state to its utility.
1871     return { [w_state, w_util(uf, expr_ref, w_state)]
1872              : w_state in w.cm().poss_states() };
1873   };
1874 
1875     w_util := procedure(uf, expr_ref, w_state) {
1876       /* Truths, or utility relevant truths, I suppose. Collect the expressions 
1877          in the rational utility function that had this w_state among its set of
1878          truthmakers / referents.  */
1879       truths := { expr : expr in domain(expr_ref) | w_state in expr_ref[expr] };
1880       // Sum the utilities 
1881       return +/ { uf[expr] : expr in truths };
1882     };
1883 
1884   /* Agential Identity
1885      -----------------
1886      Agential Identity is much like Personal Identity a la Derek Parfit's 
1887      Reasons and Persons. But where personal identity roughly concerns when 
1888      someone is the same person for the purposes of care, agential identity
1889      concerns when someone is the same agent for purposes of trusting their
1890      normative judgments. 
1891 
1892      If we are thinking in terms of ideal advisor / observer theories, we might
1893      be considering hypothetical versions of ourselves with more information 
1894      or other qualities. But consider the full knowledge of what heroin feels 
1895      like. If we had that information, we might become addicts and change our 
1896      values. But this probably isn't a change that would make us want to defer
1897      to that self's values. We may protest that something in the process of
1898      adding this knowledge has changed our values, not illuminated them.
1899      
1900      The concept of agential identity is meant to measure how much other 
1901      possible selves truly reflect *our* values and agency. Generally, this 
1902      will be measured either by similarity to our current selves or by
1903      identifying the changes as cognitive changes made through inference or
1904      applying higher-order decision criteria to values. 
1905   */
1906   agential_identity := procedure(dss, w, b) { // dss : list of decision states
1907     return 0.5 * agential_continuity(dss, w, b) +
1908            // kinda like: 0.5 * agential_connection(dss[1], {}, dss[#dss])
1909            0.5 * (0.5 * p_conn(dss[1], last(dss)) +
1910                   0.5 * u_conn(dss[1], {}, last(#dss)));
1911   };
1912   agential_continuity := procedure(dss, w, b) {
1913     conns := [agential_connection(dss[j], dss[j+1], dss[j+2], w, b, j)
1914               : j in [1..(#dss - 2)] ];
1915     return 0.5 * min(conns) + 0.5 * avg(conns);
1916   };
1917   agential_connection := procedure(ds1, ds2, ds3, w, b, t_i) {
1918     return 0.5 * avg([p_conn(ds1, ds2), p_conn(ds2, ds3)]) +
1919            0.5 * u_conn(ds1, ds2, ds3, w, b, t_i);
1920   };
1921   /* Agential continuity restricted to p_conn.
1922      Used for measuring diachronic rationality in incoherence. */
1923   p_conn_continuity := procedure(dss) {
1924     return avg({ p_conn(dss[j], dss[j+1]) : j in [1..(#dss - 1)] });
1925   };
1926   /* Measures connectedness of credences between two decision states. They
1927      are connected by either having similar probability values or by reflecting
1928      cognitive changes, i.e. updating using conditional probabilities and
1929      resulting in probability values that are close to (locally) ideally 
1930      rational inferences. */
1931   p_conn := procedure(ds1, ds2) {
1932     return avg({
1933       // Gain full credit of the higher of similarity or cognitive score and
1934       max( sim_cog_scores(ds1, ds2, p_i) ) +
1935         // Close the remaining distance proportional to
1936         (1 - max( sim_cog_scores(ds1, ds2, p_i) )) *
1937         // the other of the similarity or cognitive score
1938         min( sim_cog_scores(ds1, ds2, p_i) )
1939       // For every p var
1940       : p_i in p_vars()
1941     });
1942   };
1943 
1944     sim_cog_scores := procedure(ds1, ds2, p_i) {
1945       return [p_i_sim(ds1, ds2, p_i), cog_change(ds1, ds2, p_i)];
1946     };
1947 
1948     // Similarity / closeness. Returns 0-1.
✔1949     p_i_sim := procedure(ds1, ds2, p_i) {
1950       max_dist := max({ abs(ds1[p_i] - r_i) : r_i in r[p_i] });
1951       return 1 - abs(ds1[p_i] - ds2[id_var(p_i)]) / max_dist;
1952     };
1953 
1954     // Cognitive change. Returns 0-1.
1955     cog_change := procedure(ds1, ds2, p_i) {
1956       if (p_i in range(p)) { // rather than range(cp)
1957         return 0;
1958       } else {
1959         arr := p_inv(p_i);
1960         hyp := arr[1];
1961         evd := arr[2];
1962         ancs := non_shared_ancestors(p_i, m);
1963         if (p[hyp] in ancs && p[evd] in ancs && cp[[evd, hyp]] in ancs) {
1964           /* For simplicity we just use the p vals in the immediate parent 
1965              (ds1). Really we should construct and use 
1966              non_shared_ancestors_with_depth and pull the p values from the 
1967              correct time slice. Similarly for id_expr. */
1968 
1969           // Rational P(H|E) = P(E|H) * P(H) / P(E)
1970           rat_h_e := ds1[cp[[evd, hyp]]] * ds1[p[hyp]] / ds1[p[evd]];
1971           // Distance from rational
1972           dist_rat := abs(rat_h_e - ds2[ cp[ [id_expr(hyp), id_expr(evd)] ] ]);
1973           // Maximum distance possible
1974           max_dist := max({ abs(rat_h_e - r_i) : r_i in r[p_i] });
1975           return 1 - dist_rat / max_dist;
1976         } else {
1977           return 0;
1978         }
1979       } // end else 
1980     }; // end cog_change
1981 
1982   /* Takes an expression e and returns the expression at the next time step
1983      that would be identical. In many cases, this is just the same expression e,
1984      but we define input variables as indexicals so the same expression next
1985      time step does not refer to the expression in this time step. So, we
1986      introduce a new term At(expr, -1) which at that time step, would refer to 
1987      the same as this time's expr.  
1988   */
✔1989   id_expr := procedure(expr) {
1990     if (isList(expr)) { // in case it's called on p_inv of cp var
1991       return [ id_expr(expr_i) : expr_i in expr ];
1992     } else {
1993       if (p[expr] in i) { // current input
1994         return At_t(expr, -1);
1995       } else if (isTerm(expr) && fct(expr) == "At_t") { // past, add 1 more step
1996         return At_t(args(expr)[1], args(expr)[2] - 1);
1997       } else {
1998         return expr;
1999       }
2000     }
2001   };
2002 
2003   /* Takes a prob variable and finds its expr preimage, then finds the expr that
2004      in the next time would be identical to this expr. Returns that expr var. */
✔2005   id_var := procedure(p_var) {
2006     return p[id_expr(p_inv(p_var))];
2007   };
2008 
✔2009   poss_i_events := procedure() {
2010     return +/ { possible_states(isub, r) : isub in ne_pow(i) };
2011   };
2012 
✔2013   e_vars := procedure() {
2014     return +/ { range(n_i['e']) : n_i in n };
2015   };
2016 
✔2017   poss_ue_events := procedure() {
2018     return +/ { possible_states(ue_sub, r)
2019                 : ue_sub in ne_pow(range(u) + e_vars()) };
2020   };
2021 
✔2022   poss_p_i_events := procedure() {
2023     return +/ { { [p_i, r_i] : r_i in r[p_i] } : p_i in range(p) };
2024   };
2025 
2026   poss_p_var_events := procedure() {
2027     return +/ { { [p_i, r_i] : r_i in r[p_i] } : p_i in p_vars() };
2028   };
2029 
2030   // Possible states of all prescription vars
✔2031   poss_rx_states := procedure() {
2032     n_o_vars := +/ { n_i['o'] : n_i in n };
2033     return possible_states(n_o_vars, r);
2034   };
2035 
2036   // Possible single prescriptions for some higher-order utility
✔2037   poss_rxs := procedure() {
2038     n_os := { n_i['o'] : n_i in n };
2039     return +/ { possible_states(n_o, r) : n_o in n_os };
2040   };
2041 
2042   /* Utility Function Connectedness
2043      ------------------------------
2044      Measures how much the utility function has either remained similar or 
2045      changed as the result of a cognitive process involving i) recognition that 
2046      some prescription (rx) would cause a utility change, ii) that recognition
2047      in fact causes the prescription and iii) that prescription causes the 
2048      utility change. These are to be contrasted with changes to utilities from
2049      mere noise, associations or biases.  */
2050   u_conn := procedure(w, b, t_i, ds1, ds2, ds3) {
2051     actual_rxs := { rx : rx in poss_rxs()
2052                        | rx_to_tuple(w, b, t_i, ds1, ds2, ds3, rx) != {} };
2053     rx_subsets := pow(actual_rxs);
2054 
2055     dists := { dist_to(w, b, t_i, ds1, ds2, ds3, rx_subset)
2056                : rx_subset in rx_subsets };
2057     return 1 - min(dists);
2058   }; // end u_conn
2059 
2060     /* Takes a prescription and returns the tuples if any which realize i, ii
2061        and iii above.  */
2062     rx_to_tuple := procedure(w, b, t_i, ds1, ds2, ds3, rx) {
2063       poss_tuples := poss_p_var_events() >< poss_i_events()  ><
2064                                p_range() >< poss_ue_events();
2065       return { tuple : tuple in poss_tuples
2066                      | observed(w, b, t_i, rx, ds1, ds2, ds3, tuple) };
2067     };
2068 
2069       observed := procedure(w, b, t_i, rx, ds1, ds2, ds3, tuple) {
2070         f_p_i  := tuple[1]; // Assignment of value to p_i, rx []-> ue
2071         g_i_rx := tuple[2]; /* Assignment of value to a prescription which is
2072                                introspectively accessible as i vars */
2073         p_ue_val := tuple[3]; // Credence placed in ue (the consequent of []->)
2074         h_ue   := tuple[4]; // ue event
2075         return f_p_i != {} && g_i_rx != {} && h_ue != {} &&
2076           // g_i_rx and rx are implemented by the same brain event and 
2077           // the decision events occur at the right times
2078           lf_inv(g_i_rx) == lf_inv(rx) && restricted_eq(ds2, g_i_rx) &&
2079           restricted_eq(ds2, rx) && restricted_eq(ds1, f_p_i) &&
2080           restricted_eq(ds3, h_ue) &&
2081           // first(domain(f_p_i)) is p_i and p_i is _ []-> _
2082           fct(p_var_inv(first(domain(f_p_i)))) == "BoxArrow" &&
2083           /* The ref of the brain event of ds1 implementing the placement of 
2084              prob in the p_i expr == lf_inv h_ue in two time steps
2085              i.e. the consequent of []-> refers to the intended ue change */
2086           /* Todo: Allow for changes that had i, ii, and iii but only partially 
2087              updated the utility / eval functions.  */
2088           ref(w,b)[lf_inv_at(b, t_i)[
2089             {[ p[args(p_var_inv(first(domain(f_p_i))))[2]], p_ue_val ]}
2090           ]] == lf_inv_at(b, t_i + 2)[h_ue] &&
2091           // p_i influences each var in rx
2092           first(domain(f_p_i)) in { parents(v) : v in domain(rx) } &&
2093           // each var in rx influences each var in the utility change 
2094           forall(v in g_i_rx | v in { parents(ue) : ue in domain(h_ue) });
2095       };
2096 
2097     /* Given a subset of observed prescriptions, we compare the resulting 
2098        utility function to what was prescribed within that subset. The overall 
2099        u_conn score will take the minimum distance seen this way.
2100          Todo: Allow for changes that had i, ii, and iii but only partially 
2101        updated the utility / eval functions.  */
2102     dist_to := procedure(w, b, t_i, ds1, ds2, ds3, rx_subset) {
2103       u1 := { [u_i, ds1[u_i]] : u_i in u };
2104       e1 := { u1 } + { { [e_i, ds1[e_i]] : e_i in n_i['e'] } : n_i in n };
2105 
2106       rxd := { [e_i, rx_e_i_val(w, b, t_i, ds1, ds2, ds3, rx_subset, e_i)]
2107                : e_i in domain(e1) };
2108       rxd_u := { [u_i, rxd[u_i]] : u_i in u };
2109       rxd_n := [ { [e_i, rxd[e_i]] : e_i in n_i['e'] } : n_i in n ];
2110       rxd_e := [ rxd_u ] + rxd_n;
2111       // The prescribed util / eval change
2112       ord_rxd_e := [ additive_to_ordinal(rxd_e[j], j, ue_state_space())
2113                      : j in [1..#rxd_e] ];
2114       // The actual change in ds3
2115       ord_e := [ additive_to_ordinal(e_func(ds3, j), j, ue_state_space())
2116                  : j in [1..#rxd_e] ];
2117 
2118       e_dists := [ ord_u_dist(ord_e[j], ord_rxd_e[j]) : j in [1..#ord_e] ];
2119 
2120       // Todo: Add weights? 
2121       return avg(e_dists);
2122     }; // end dist_to
2123 
2124       /* Given a subset of observed prescriptions and an e_i var, return the
2125          value prescribed for the e_i var.  */
2126       rx_e_i_val := procedure(w, b, t_i, ds1, ds2, ds3, rx_subset, e_i) {
2127         /* The prescribed values (rxds) are the values of the e_i var in the 
2128            ue event from rx_to_tuple (for any rxs that prescribe for e_i). */
2129         rxds := { rx_to_tuple(w, b, t_i, ds1, ds2, ds3, rx_i)[4][e_i]
2130           : rx_i in rx_subset  // h_ue[e_i]
2131           | e_i in domain(rx_to_tuple(w, b, t_i, ds1, ds2, ds3, rx_i)[4]) };
2132             // e_i in domain(h_ue)
2133         if (#rxds > 0) {
2134           // If #rxds > 1, they should all be the same anyway bc it was observed
2135           return first(rxds);
2136           /* Todo: In later versions, we probably want to allow for non-exact 
2137              changes and then choose the one closest to the observed.  */
2138         } else {
2139           return e1[e_i]; // No change
2140         }
2141       };
2142 
2143   // Utility / Evaluation Function implemented in a given decision state ds
✔2144   e_func := procedure(ds, j) {
2145     if (j == 0) {
2146       return { [u_i, ds[u_i]] :  u_i in range(u) };
2147     } else {
2148       return { [e_i, ds[e_i]] : e_i in range(n[j]['e']) };
2149     }
2150   };
2151 
✔2152   ue := procedure(j) {
2153     if (j == 0) {
2154       return u;
2155     } else {
2156       return n[j]['e'];
2157     }
2158   };
2159 
✔2160   ue_base_exprs := procedure(j) {
2161     return +/ { subformulas(x_i) : x_i in domain(ue(j)) };
2162   };
2163 
2164   /* Takes a decision state, i.e. a function from (among other things) utility
2165      variables to numbers (utilities), and an index j and returns a set of 
2166      SuccEq (succeeds or equals) setlx functors. If j is 0, then u is converted
2167      to ordinal, otherwise, n[j]['e'] is. */
2168   additive_to_ordinal := procedure(ds, j, state_space) {
2169     card_u := add_u_to_card_u(e_func(ds,j), state_space);
2170     return card_u_to_ord_u( card_u, domain(card_u), r[first(p)] );
2171   };
2172 
2173   /* Brain-State Measure Paths 
2174      -------------------------
2175      Returns a list where for each future time, there is a set of 
2176      bs_msr_paths, each of which in turn is a list of bs_msrs for each time 
2177      from the first to the given time. A bs_msr is a pair [bs, msr]. 
2178     
2179      One can think in terms of a tree. At the root is the given starting brain 
2180      state. Each branch is a continuation with different inputs and a measure 
2181      for that branch based on subjective likelihood. A path is a full branch 
2182      line from root to leaf collecting pairs of brain states and measures along
2183      the way. 
2184 
2185      e.g. [bs_msr_paths_t1, ..., bs_msr_paths_tz]
2186        bs_msr_paths_tj := { bs_msrs_tj_1, bs_msr_tj_2, ... }
2187          bs_msrs_tj_k := [ bs_msr_t1, ..., bs_msr_tj ]
2188            bs_msr_tj := [bs_tj, msr]
2189 
2190                      [ bs1, 1 ]
2191                     /   |      \
2192                is1 /    |is2    \  is3   (input states leading to continuations)
2193                   /     |        \  
2194                  /      |         \
2195      [bs_t2a, 1/6]  [bs_t2b, 1/2]  [bs_t2c, 1/3]  
2196       /    |    \     /   |   \      /   |   \
2197      ...
2198 
2199      There's some duplication and space inefficiency in having the previous 
2200      times' brain states and measures present both in the earlier elements of
2201      the top level list as well as within the set of paths for each element.
2202      We probably could do without it but it makes it a little more convenient
2203      when calculating the voter weights for each time's voters in computing
2204      the rational utility function. Some aspects of those weights like the 
2205      agential identity depend on the entire path taken and not just the final
2206      brain state.
2207   */
2208   bs_msr_paths := procedure(w, b, bs1, t_j) {
2209     if (t_j == 1) {
2210       return [{[[bs1, 1]]}];
2211     } else {
2212       return bs_msr_paths(w, b, bs1, t_j - 1) +
2213         [+/ {
2214            { bmp + [bs_msr]
2215              : bs_msr in next_bs_msrs(w, b, last(bmp)[1], last(bmp)[2], t_j-1) }
2216            : bmp in last(bs_msr_paths(w, b, bs1, t_j - 1))
2217          }];
2218     }
2219   };
2220 
2221   /* Takes a brain, brain state, measure and prev t_i and returns the possible
2222      continuations in the next time step together with their measure 
2223      roughly proportional to the subjective likelihood.  */
2224   next_bs_msrs := procedure(w, b, bs_i, msr, t_j) {
2225     bs_j := b.response(bs_i);
2226     // Possible brain input states from each di possible decision input states.
2227     pbis := { [di, lf_inv(b)[di]] : di in poss_i_states() };
2228     /* Possibly empty brain input states since we now filter by compatibility
2229        with the brain response bs_j. (Recall that input vars may overlap with
2230        other vars that bs_j may dictate values for.) */
2231     pe_bis := { [di, { pbi : pbi in pbi_s | compat(pbi, bs_j) }]
2232                 : [di, pbi_s] in pbis };
2233     // pbi_s = possible brain input sets
2234     bis := { [di, pbi_s] : [di, pbi_s] in pe_bis | pbi_s != {} };
2235 
2236     /* For each brain input state of each decision input state, map the total
2237        brain state including the response bs_j to its new measure. 
2238 
2239        Ideally, the new measure would be proportional to the brain input 
2240        state's subjective probability. This was under development but doing it 
2241        in a way that is biologically plausible presents a challenge. To avoid 
2242        an implausible number of explicit probabilities, we'd probably have to 
2243        look at the closest coherent extensions of the current probability 
2244        distribution as well as allow for indirect reference, which introduces 
2245        its own challenges in translating probabilities from direct to indirect.
2246        
2247        Although I by no means think these challenges insurmountable, the 
2248        technical complications involved seemed too great for a first version
2249        and not worth delaying the initial release over. As a placeholder here,
2250        we simply assume each possible decision input state is equally probable
2251        and each brain state implementing a given decision input state is
2252        similarly equally probable to other such implementations.
2253 
2254        While incorporating the subjective probability seems preferable, it's
2255        also worth mentioning that it may not actually be necessary. The main
2256        motivation is to make continuations of the agent under very weird 
2257        scenarios matter less. But if the worry there is that those 
2258        circumstances are distorting the agent's values, we already have the 
2259        agential_identity measure to discount them. In other words, agential
2260        identity may screen off a circumstance's weirdness from its relevance.
2261     */
2262     return +/ {
2263       { [ bi + bs_j, msr * (1 / #domain(bis)) * (1 / #bis[di]) ]
2264         : bi in bis[di] }
2265       : di in domain(bis)
2266     };
2267   };
2268 
2269 
2270 // Class Methods
2271 // =============
2272 
2273   static {
2274     /* Function from a causal_model of a brain b and a set of decision 
2275        algorithm candidates to the decision algorithm that is the best 
2276        compression of the brain.  */
2277     implemented_by := cachedProcedure(b, ds) {
2278       if (ds == {}) {
2279         ds := decision_algorithm.all(b);
2280       }
2281       /* Requiring simplest version helps ensure higher-order ambitiousness,
2282          i.e. prevents smuggling in higher-order norms within the n[j]['m2'] 
2283          variables. In future iterations, this might be softened.  */
2284       ds := [d : d in ds | d.is_implemented_by(b) && d.is_simplest_version(b)];
2285       ds := sort_list(ds, decision_algorithm.better_explanation(b));
2286       return ds[1];
2287     };
2288 
2289     /* Given a causal model of a brain, return the set of possible decision 
2290        algorithms which could be implemented by it based simply on number of 
2291        states. A decision algorithm can't be more fine-grained than its 
2292        substrate.  */
2293     all := cachedProcedure(b) {
2294       return { d : d in decision_algorithm.all_lte(#b.poss_states()) };
2295     };
2296 
2297     // All with #poss_states <= z
2298     // Todo: Add possible At_t exprs and predicates and quantifiers
2299     all_lte := cachedProcedure(z) {
2300       poss_i := da().ltr_up_to('I', z/2);
2301       var_ltrs := { 'A', 'B', 'C' };
2302       poss_base_vars := da().vars_up_to(var_ltrs, n);
2303       poss_exprs := { da().add_up_to(pbe, z/2)
2304                       : pbe in poss_base_vars };
2305       poss_p := da().poss_expr_to_ltr(poss_exprs, 'P');
2306       // e.g. { [[x, y], 'P(x|y)'], ... } 
2307       poss_cp := pow({ [[x, y], 'P(' + str(x) + '|' + str(y) + ')']
2308                        : [x, y] in poss_exprs >< poss_exprs });
2309       poss_o := da().ltr_up_to('O', z/2);
2310       poss_u := da().poss_expr_to_ltr(poss_exprs, 'U');
2311       poss_m := da().ltr_up_to('M', z/2);
2312       poss_m2 := da().ltr_up_to('M2', z/2);
2313       poss_n := +/ { choices({ da().poss_nj(poss_exprs, z, j) : j in [1..x] })
2314                      : x in [1..z] };
2315       return +/ {
2316         +/ { da().poss_ds(d_i, d_o, d_p, d_cp, d_u, d_m, d_m2, d_n, poss_r)
2317              : poss_r in da().poss_rs(z, d_i, d_o, d_p, d_cp,
2318                                          d_u, d_m, d_m2, d_n) }
2319         : [d_i, d_o, d_p, d_cp, d_u, d_m, d_m2, d_n] in
2320           da().cart_prod(poss_i, poss_o, poss_p, poss_cp,
2321                          poss_u, poss_m, poss_m2, poss_n)
2322       };
2323     }; // end all_lte
2324 
✔2325       ltr_up_to := procedure(ltr, j) {
2326         return { ltr + '_' + y : y in [1..j] };
2327       };
2328 
✔2329       vars_up_to := procedure(ltrs, j) {
2330         return +/ { da().ltr_up_to(ltr, j) : ltr in ltrs };
2331       };
2332 
2333       add_one := procedure(exprs) {
2334         unary := { 'Not' };
2335         binary := { 'And', 'Or', 'Implies', 'BoxArrow' };
2336         add_un := { makeTerm(op, [expr]) : [op, expr] in unary >< exprs };
2337         add_bi := { makeTerm(op, [expr1, expr2])
2338                     : [op, [expr1, expr2]] in binary >< (exprs >< exprs) };
2339         return exprs + add_un + add_bi;
2340       };
2341 
2342       add_up_to := procedure(base_vars, j) {
2343         if (j == 0) {
2344           return base_vars;
2345         } else {
2346           return da().add_one( da().add_up_to(base_vars, j - 1) );
2347         }
2348       };
2349 
✔2350       expr_to_ltr_var := procedure(expr, ltr) {
2351         return ltr + '(' + replace(str(expr), '"', '') + ')';
2352       };
2353 
2354       poss_expr_to_ltr := procedure(poss_exprs, ltr) {
2355         return { { [expr, da().expr_to_ltr_var(expr, ltr)] : expr in subset }
2356                  : subset in pow(poss_exprs) };
2357       };
2358 
2359       poss_nj := procedure(poss_exprs, z, j) {
2360         poss_e_nj := da().poss_expr_to_ltr(poss_exprs, 'E_n' + j);
2361         poss_m2_nj := da().ltr_up_to('M2_n' + j, z/2);
2362         poss_o_nj := da().ltr_up_to('O_n' + j, z/2);
2363         return { { ['e', e_n], ['m', m_n], ['o', o_n] }
2364           : [e_n, m_n, o_n] in cart_prod([poss_e_nj, poss_m2_nj, poss_o_nj]) };
2365       };
2366 
2367       poss_rs := procedure(z, d_i, d_o, d_p, d_cp, d_u, d_m, d_m2, d_n) {
2368         poss_p_vals := { { j / x : j in [0..x] } : x in [1..z] };
2369         poss_ue_vals := ne_pow({ j : j in [1..2**z] });
2370         poss_z_vals := { { j : j in [1..x] } : x in [1..z] };
2371         poss_o_vals := poss_z_vals;
2372 
2373         poss_r_ps := {
2374           { [i_var,  p_vals] : i_var  in d_i         } +
2375           { [p_var,  p_vals] : p_var  in range(d_p)  } +
2376           { [cp_var, p_vals] : cp_var in range(d_cp) }
2377           : p_vals in poss_p_vals
2378         };
2379 
2380         return +/ choices(
2381           { poss_r_ps, da().poss_r_ue(poss_ue_vals, d_u) } +
2382           { da().poss_r_ue(poss_ue_vals, n_i['e']) : n_i in d_n } +
2383           { da().poss_r_z(poss_z_vals, d_z) : d_z in { d_o, d_m, d_m2 } }
2384         );
2385       }; // end poss_rs
2386 
✔2387         poss_r_ue := procedure(poss_ue_vals, ue) {
2388           return { { [ue_var, ue_vals] : ue_var in range(ue) }
2389                    : ue_vals in poss_ue_vals };
2390         };
2391 
✔2392         poss_r_z := procedure(poss_z_vals, d_z) {
2393           return choices({ {z_var} >< poss_z_vals : z_var in d_z });
2394         };
2395 
2396       poss_ds := procedure(z, d_i, d_o, d_p, d_cp, d_u, d_m, d_m2, d_n, d_r) {
2397         poss_is_state := possible_states(d_i + d_p + d_cp +
2398                                          d_u + d_m + d_m2 + d_n, d_r);
2399         poss_s_state  := possible_states(d_p + d_cp + d_u +
2400                                          d_m + d_m2 + d_n, d_r);
2401         poss_t_s := function_space(poss_is_state, poss_s_state);
2402 
2403         poss_p_u_m2 := possible_states(d_p + d_u + d_m2, d_r);
2404         poss_o_state := possible_states(d_o, d_r);
2405         poss_t_o := function_space(poss_p_u_m2, poss_o_state);
2406 
2407         das := {
2408           decision_algorithm(d_i, d_o, d_p, d_cp, d_u, d_m, d_m2, d_n,
2409                              d_r, d_t_s, d_t_o, om, om, om)
2410           : [d_t_s, d_t_o] in poss_t_s >< poss_t_o
2411         };
2412         return { da : da in das | da.is_valid() && #da.poss_states() <= z};
2413       };
2414 
2415     better_explanation := cachedProcedure(b) {
2416       return procedure(d1, d2) {
2417                return da().expl_score(b, d1) > da().expl_score(b, d2);
2418              };
2419     };
2420 
2421       expl_score := procedure(b, d_i) {
2422         return d_i.ambitiousness(b) - d_i.complexity(b)
2423                - d_i.instr_irrat(b) - d_i.incoherence(b);
2424       };
2425 
2426     simpler := cachedProcedure() {
2427       return procedure(d1, d2) {
2428                return k(d1.to_s) < k(d2.to_s);
2429              };
2430     };
2431 
✔2432     new := procedure() {
2433       return decision_algorithm({}, {}, {}, {}, {}, {}, {}, [], {}, {}, {},
2434                                 om, om, om);
2435     };
2436 
2437   }
2438 }
2439 
2440 // alias 
2441 da := procedure() { return decision_algorithm; };