Generating Equations

Mainly to test correctness of equations generated along with forward evolution

In [1]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.0`
Out[1]:
import $ivy.$
In [2]:
import provingground._ , interface._, HoTT._
import learning._
import library._, MonoidSimple._
Out[2]:
import provingground._ , interface._, HoTT._

import learning._

import library._, MonoidSimple._
In [ ]:
In [3]:
repl.pprinter.bind(translation.FansiShow.fansiPrint)
In [4]:
val tg = TermGenParams()
tg.nodeCoeffSeq
Out[4]:
tg: TermGenParams = TermGenParams(0.1, 0.1, 0.1, 0.1, 0.1, 0.05, 0.05, 0.05, 0.3, 0.7, 0.5)
res3_1: NodeCoeffSeq[TermState, Term, Double] = Cons(
  BaseCons(
    BasePi(provingground.learning.RandomVarFamily$$Lambda$2292/368952730@30d6b608, FuncsWithDomain),
    0.55,
    BaseCons(
      BasePi(provingground.learning.GeneratorNode$$Lambda$2295/1777621063@ff038da, FuncsWithDomain),
      0.1,
      BaseCons(
        BasePi(
          provingground.learning.GeneratorNode$$Lambda$2295/1777621063@3c109d59,
          FuncsWithDomain
        ),
        0.1,
        BaseCons(
          BasePi(
            provingground.learning.GeneratorNode$$Lambda$2295/1777621063@55e999c2,
            FuncsWithDomain
          ),
          0.1,
          BaseCons(
            BasePi(
              provingground.learning.TermGeneratorNodes$$Lambda$2281/168572575@7d28562a,
              FuncsWithDomain
            ),
            0.1,
            Target(FuncsWithDomain)
          )
        )
      )
    )
  ),
  Cons(
    BaseCons(
      Map(
        provingground.learning.TermRandomVars$TargetTyps$$$Lambda$2298/413538804@619b999d,
        Goals,
        TargetTyps
      ),
      0.7,
      BaseCons(
        Map(
          provingground.learning.TermRandomVars$TargetTyps$$$Lambda$2299/1742855736@64d6a6f1,
          Typs,
          TargetTyps
        ),
        0.30000000000000004,
        Target(TargetTyps)
      )
    ),
...
In [5]:
val mfd = MonixFiniteDistributionEq(tg.nodeCoeffSeq)
val ts = TermState(dist1, dist1.map(_.typ))
Out[5]:
mfd: MonixFiniteDistributionEq[TermState, Term] = MonixFiniteDistributionEq(
  Cons(
    BaseCons(
      BasePi(
        provingground.learning.RandomVarFamily$$Lambda$2292/368952730@30d6b608,
        FuncsWithDomain
      ),
      0.55,
      BaseCons(
        BasePi(
          provingground.learning.GeneratorNode$$Lambda$2295/1777621063@ff038da,
          FuncsWithDomain
        ),
        0.1,
        BaseCons(
          BasePi(
            provingground.learning.GeneratorNode$$Lambda$2295/1777621063@3c109d59,
            FuncsWithDomain
          ),
          0.1,
          BaseCons(
            BasePi(
              provingground.learning.GeneratorNode$$Lambda$2295/1777621063@55e999c2,
              FuncsWithDomain
            ),
            0.1,
            BaseCons(
              BasePi(
                provingground.learning.TermGeneratorNodes$$Lambda$2281/168572575@7d28562a,
                FuncsWithDomain
              ),
              0.1,
              Target(FuncsWithDomain)
            )
          )
        )
      )
    ),
    Cons(
      BaseCons(
        Map(
          provingground.learning.TermRandomVars$TargetTyps$$$Lambda$2298/413538804@619b999d,
          Goals,
          TargetTyps
        ),
        0.7,
        BaseCons(
          Map(
            provingground.learning.TermRandomVars$TargetTyps$$$Lambda$2299/1742855736@64d6a6f1,
...
ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(e_l, 0.047619047619047616),
      Weighted(e_r, 0.047619047619047616),
      Weighted(mul, 0.047619047619047616),
      Weighted(eqM, 0.047619047619047616),
      Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
      Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.047619047619047616),
      Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
      Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
      Weighted(eqM, 0.2857142857142857),
      Weighted(mul, 0.2857142857142857)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.047619047619047616),
      Weighted(M, 0.047619047619047616),
      Weighted((M → (M → M)), 0.047619047619047616),
      Weighted((M → (M → 𝒰 )), 0.047619047619047616),
      Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
      Weighted(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.047619047619047616),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.047619047619047616
      ),
      Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
      Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
      Weighted((M → (M → 𝒰 )), 0.2857142857142857),
      Weighted((M → (M → M)), 0.2857142857142857)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
In [6]:
import TermRandomVars._
val tsk = mfd.varDist(ts)(Terms, 0.001)
import monix.execution.Scheduler.Implicits.global
Out[6]:
import TermRandomVars._

tsk: monix.eval.Task[(FiniteDistribution[Term], Set[GeneratorVariables.EquationTerm])] = FlatMap(
  Async(<function2>, true, true, true),
  monix.eval.Task$$Lambda$2530/1333989368@294e856f
)
import monix.execution.Scheduler.Implicits.global
In [7]:
val rp = tsk.runSyncUnsafe()
val eqs = rp._2
Out[7]:
rp: (FiniteDistribution[Term], Set[GeneratorVariables.EquationTerm]) = (
  FiniteDistribution(
    Vector(
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.029778252577854582),
      Weighted(mul(e_r)(e_l), 0.0053934227946860315),
      Weighted(eqM(e_r)(e_r), 0.0053934227946860315),
      Weighted((_ : ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }) ↦ eqM, 0.0011761943024481748),
      Weighted((_ : (M → (M → M))) ↦ axiom_{eqM(mul(e_l)(a))(a)}, 0.0011761943024481746),
      Weighted((_ : ∏(a : M){ eqM(a)(a) }) ↦ mul, 0.0011761943024481748),
      Weighted(eqM(e_r)(e_l), 0.0053934227946860315),
      Weighted((_ : (M → (M → 𝒰 ))) ↦ axiom_{eqM(mul(a)(e_r))(a)}, 0.0011761943024481746),
      Weighted(mul(e_r), 0.02478994011666693),
      Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.029778252577854582),
      Weighted((_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ mul, 0.0011761943024481748),
      Weighted((@a : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ @a, 0.0015122498174333678),
      Weighted((@a : (M → (M → 𝒰 ))) ↦ @a(e_r), 0.0023589908047798197),
      Weighted((_ : (M → (M → 𝒰 ))) ↦ e_l, 0.0011761943024481746),
      Weighted(eqM(e_l)(e_l), 0.0053934227946860315),
      Weighted(
        (_ : (M → (M → 𝒰 ))) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.0011761943024481746
      ),
      Weighted((@a : (M → (M → 𝒰 ))) ↦ @a(e_l), 0.0023589908047798197),
      Weighted(axiom_{eqM(mul(a)(e_r))(a)}(e_r), 0.003541420016666704),
      Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.029778252577854582),
      Weighted(
        (_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ mul,
        0.0011761943024481748
      ),
      Weighted(mul, 0.24983231236562614),
      Weighted(eqM(e_r), 0.02478994011666693),
      Weighted(
        (@a : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ @a,
        0.0015122498174333675
      ),
      Weighted((_ : (M → (M → 𝒰 ))) ↦ eqM, 0.008233360117137222),
      Weighted(axiom_{eqM(a)(a)}(e_r), 0.003541420016666704),
      Weighted(
        (_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ eqM,
        0.0011761943024481748
      ),
      Weighted((@a : M) ↦ @a, 0.0030244996348667355),
      Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_l), 0.003541420016666704),
      Weighted((@a : (M → (M → 𝒰 ))) ↦ @a, 0.010585748722033573),
      Weighted((@a : ∏(a : M){ eqM(a)(a) }) ↦ @a, 0.0015122498174333678),
      Weighted((_ : (M → (M → M))) ↦ axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.0011761943024481746),
      Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.029778252577854582),
      Weighted(e_l, 0.033331339533166776),
      Weighted(axiom_{eqM(a)(a)}, 0.029778252577854582),
...
eqs: Set[GeneratorVariables.EquationTerm] = Set(
  EquationTerm(
    FinalVal(
      Elem(
        Wrap((_ : (M → (M → M))) ↦ axiom_{eqM(mul(a)(e_r))(a)}),
        AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
      )
    ),
    Product(
      Coeff(
        Island(
          AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
          ConstRandVar(Terms),
          AddVar((M → (M → M)), 0.3),
          Lambda,
          InIsle
        ),
        AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
      ),
      FinalVal(
        InIsle(
          Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
          @a,
          Island(
            AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
            ConstRandVar(Terms),
            AddVar((M → (M → M)), 0.3),
            Lambda,
            InIsle
          )
        )
      )
    )
  ),
  EquationTerm(
    FinalVal(Elem((@a : (M → (M → M))) ↦ @a, Terms)),
    Product(
      Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
      FinalVal(
        InIsle(
          Elem(@a, Terms),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
        )
      )
    )
  ),
  EquationTerm(
    FinalVal(
...
In [8]:
eqs
Out[8]:
res7: Set[GeneratorVariables.EquationTerm] = Set(
  EquationTerm(
    FinalVal(
      Elem(
        Wrap((_ : (M → (M → M))) ↦ axiom_{eqM(mul(a)(e_r))(a)}),
        AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
      )
    ),
    Product(
      Coeff(
        Island(
          AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
          ConstRandVar(Terms),
          AddVar((M → (M → M)), 0.3),
          Lambda,
          InIsle
        ),
        AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
      ),
      FinalVal(
        InIsle(
          Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
          @a,
          Island(
            AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
            ConstRandVar(Terms),
            AddVar((M → (M → M)), 0.3),
            Lambda,
            InIsle
          )
        )
      )
    )
  ),
  EquationTerm(
    FinalVal(Elem((@a : (M → (M → M))) ↦ @a, Terms)),
    Product(
      Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
      FinalVal(
        InIsle(
          Elem(@a, Terms),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
        )
      )
    )
  ),
  EquationTerm(
    FinalVal(
...
In [9]:
val lefts = eqs.map(_.lhs)
lefts.size
Out[9]:
lefts: Set[GeneratorVariables.Expression] = Set(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  FinalVal(
    Elem(
      ((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ),
  FinalVal(
...
res8_1: Int = 585
In [10]:
import GeneratorVariables._, Expression._
val eqgs = Equation.group(eqs)
Out[10]:
import GeneratorVariables._

eqgs: Set[Equation] = Set(
  Equation(
    FinalVal(
      Elem(
        Wrap((_ : (M → (M → M))) ↦ axiom_{eqM(mul(a)(e_r))(a)}),
        AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
      )
    ),
    Product(
      Coeff(
        Island(
          AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
          ConstRandVar(Terms),
          AddVar((M → (M → M)), 0.3),
          Lambda,
          InIsle
        ),
        AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
      ),
      FinalVal(
        InIsle(
          Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
          @a,
          Island(
            AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
            ConstRandVar(Terms),
            AddVar((M → (M → M)), 0.3),
            Lambda,
            InIsle
          )
        )
      )
    )
  ),
  Equation(
    FinalVal(
      InIsle(
        Elem(mul, Terms),
        @a,
        Island(
          Terms,
          ConstRandVar(Terms),
          AddVar(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }, 0.3),
          Lambda,
          InIsle
        )
      )
    ),
    Product(
...
In [11]:
eqgs.size
eqs.size
Out[11]:
res10_0: Int = 585
res10_1: Int = 809
In [12]:
eqgs.head
Out[12]:
res11: Equation = Equation(
  FinalVal(
    Elem(
      Wrap((_ : (M → (M → M))) ↦ axiom_{eqM(mul(a)(e_r))(a)}),
      AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
    )
  ),
  Product(
    Coeff(
      Island(
        AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
        ConstRandVar(Terms),
        AddVar((M → (M → M)), 0.3),
        Lambda,
        InIsle
      ),
      AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
    ),
    FinalVal(
      InIsle(
        Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
        @a,
        Island(
          AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
          ConstRandVar(Terms),
          AddVar((M → (M → M)), 0.3),
          Lambda,
          InIsle
        )
      )
    )
  )
)
In [13]:
eqgs.map(_.rhs)
Out[13]:
res12: Set[Expression] = Set(
  Sum(
    Sum(
      Product(
        Product(Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms), FinalVal(Elem((M → (M → M)), Typs))),
        FinalVal(Elem((_ : (M → (M → M))) ↦ axiom_{eqM(mul(a)(e_r))(a)}, Terms))
      ),
      Product(
        Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
        FinalVal(
          InIsle(
            Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
            @a,
            Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
          )
        )
      )
    ),
    Product(
      Coeff(BaseThenCondition(FlatMap(Typs, LambdaIsle, Terms), Funcs, Restrict(FuncOpt)), Funcs),
      FinalVal(
        InIsle(
          Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
        )
      )
    )
  ),
  Product(
    Coeff(
      FlatMap(
        Typs,
        provingground.learning.TermGeneratorNodes$$Lambda$2283/1598454918@70bec38a,
        Typs
      ),
      Typs
    ),
    FinalVal(
      InIsle(
        Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar((M → (M → 𝒰 )), 0.3), Sigma, InIsle)
      )
    )
  ),
  Product(
    Coeff(Init(Terms), Terms),
...
In [14]:
val rights = eqgs.map(_.rhs).flatMap(GeneratorVariables.Expression.varVals)
Out[14]:
rights: Set[VarVal[_]] = Set(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  InitialVal(
    InIsle(
      Elem(e_l, Terms),
      @a,
      Island(
        AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
        ConstRandVar(Terms),
...
In [15]:
val extras = rights -- lefts.flatMap(GeneratorVariables.Expression.varVals)
Out[15]:
extras: Set[VarVal[_]] = Set(
  InitialVal(Elem(mul, Terms)),
  InitialVal(Elem(e_r, Terms)),
  InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)),
  InitialVal(
    Elem(
      Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}),
      AtCoord(FuncsWithDomain, M :: HNil)
    )
  ),
  InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(eqM, AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil))),
  InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), Funcs)),
  InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)),
  InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
  InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }, Typs)),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem((M → (M → M)), Typs)),
  InitialVal(Elem(eqM, Terms)),
  InitialVal(Elem(∏(a : M){ eqM(mul(a)(e_r))(a) }, Typs)),
  InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs)),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), Funcs)),
  InitialVal(Elem(Wrap(eqM), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, Typs)),
  InitialVal(Elem(M, Typs)),
  InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(Wrap(@a), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(Wrap(mul), Funcs)),
  InitialVal(Elem(Wrap(@a), Funcs)),
  InitialVal(Elem(axiom_{eqM(mul(e_l)(a))(a)}, Terms)),
  InitialVal(Elem(Wrap(mul), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(∏(a : M){ eqM(a)(a) }, Typs)),
  InitialVal(Elem(e_r, AtCoord(TermsWithTyp, M :: HNil))),
  InitialVal(Elem(mul, AtCoord(TermsWithTyp, (M → (M → M)) :: HNil))),
  InitialVal(Elem((M → (M → 𝒰 )), Typs)),
  InitialVal(Elem(e_l, AtCoord(TermsWithTyp, M :: HNil))),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)),
...
In [16]:
extras.size
Out[16]:
res15: Int = 46
In [17]:
lefts.size
rights.size
Out[17]:
res16_0: Int = 585
res16_1: Int = 459
In [18]:
lefts.take(20)
Out[18]:
res17: Set[Expression] = Set(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  FinalVal(
    Elem(
      ((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ),
  FinalVal(
...
In [19]:
import GeneratorVariables.Expression.varVals
val egEq = eqgs.find(eq => varVals(eq.rhs).intersect(extras).nonEmpty)
Out[19]:
import GeneratorVariables.Expression.varVals

egEq: Option[Equation] = Some(
  Equation(
    InitialVal(
      InIsle(
        Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar((M → (M → M)), 0.3), Sigma, InIsle)
      )
    ),
    Product(
      IsleScale(@a, Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
      InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs))
    )
  )
)
In [20]:
egEq.get.lhs
Out[20]:
res19: Expression = InitialVal(
  InIsle(
    Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
    @a,
    Island(Typs, ConstRandVar(Typs), AddVar((M → (M → M)), 0.3), Sigma, InIsle)
  )
)
In [21]:
egEq.get.toString
Out[21]:
res20: String = "(P\u2080(InIsle((a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs,@a,Island(Typs,Typs,AddVar,Sigma,InIsle)))) == ((IsleScale(@a,(a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs)) * (P\u2080((a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs)))"
In [22]:
varVals(egEq.get.rhs)
varVals(egEq.get.rhs).intersect(extras)
Out[22]:
res21_0: Set[VarVal[_]] = Set(InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)))
res21_1: Set[VarVal[_]] = Set(InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)))

Note: This may not be an error as we may simply have too low cutoff to get any terms on the rhs.

As we see below (which will change after a corrections), most of the extras are initial values in islands, which should be paired with those outside.

In [23]:
val initExtras = extras.filter(_.isInstanceOf[InitialVal[_]])
Out[23]:
initExtras: Set[VarVal[_]] = Set(
  InitialVal(Elem(mul, Terms)),
  InitialVal(Elem(e_r, Terms)),
  InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)),
  InitialVal(
    Elem(
      Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}),
      AtCoord(FuncsWithDomain, M :: HNil)
    )
  ),
  InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(eqM, AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil))),
  InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), Funcs)),
  InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)),
  InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
  InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }, Typs)),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem((M → (M → M)), Typs)),
  InitialVal(Elem(eqM, Terms)),
  InitialVal(Elem(∏(a : M){ eqM(mul(a)(e_r))(a) }, Typs)),
  InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs)),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), Funcs)),
  InitialVal(Elem(Wrap(eqM), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, Typs)),
  InitialVal(Elem(M, Typs)),
  InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(Wrap(@a), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(Wrap(mul), Funcs)),
  InitialVal(Elem(Wrap(@a), Funcs)),
  InitialVal(Elem(axiom_{eqM(mul(e_l)(a))(a)}, Terms)),
  InitialVal(Elem(Wrap(mul), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(∏(a : M){ eqM(a)(a) }, Typs)),
  InitialVal(Elem(e_r, AtCoord(TermsWithTyp, M :: HNil))),
  InitialVal(Elem(mul, AtCoord(TermsWithTyp, (M → (M → M)) :: HNil))),
  InitialVal(Elem((M → (M → 𝒰 )), Typs)),
  InitialVal(Elem(e_l, AtCoord(TermsWithTyp, M :: HNil))),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)),
...
In [24]:
initExtras.size
Out[24]:
res23: Int = 46
In [25]:
extras.size
Out[25]:
res24: Int = 46
In [26]:
lefts.filter(_.isInstanceOf[InitialVal[_]])
Out[26]:
res25: Set[Expression] = Set(
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  InitialVal(
    InIsle(
      Elem(e_l, Terms),
      @a,
      Island(
        AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
        ConstRandVar(Terms),
        AddVar((M → (M → 𝒰 )), 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  InitialVal(
    InIsle(
      Elem(Wrap(@a), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  InitialVal(
    InIsle(
      Elem(e_r, Terms),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(a)(a) }, 0.3), Lambda, InIsle)
    )
  ),
  InitialVal(
...
In [27]:
val linits = eqgs.filter(_.lhs.isInstanceOf[InitialVal[_]])
Out[27]:
linits: Set[Equation] = Set(
  Equation(
    InitialVal(
      InIsle(
        Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar((M → (M → M)), 0.3), Sigma, InIsle)
      )
    ),
    Product(
      IsleScale(@a, Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
      InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs))
    )
  ),
  Equation(
    InitialVal(
      InIsle(
        Elem(e_r, Terms),
        @a,
        Island(
          AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
          ConstRandVar(Terms),
          AddVar((M → (M → M)), 0.3),
          Lambda,
          InIsle
        )
      )
    ),
    Product(IsleScale(@a, Elem(e_r, Terms)), InitialVal(Elem(e_r, Terms)))
  ),
  Equation(
    InitialVal(
      InIsle(
        Elem(mul, Terms),
        @a,
        Island(
          AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
          ConstRandVar(Terms),
          AddVar((M → (M → M)), 0.3),
          Lambda,
          InIsle
        )
      )
    ),
    Product(IsleScale(@a, Elem(mul, Terms)), InitialVal(Elem(mul, Terms)))
  ),
  Equation(
    InitialVal(
      InIsle(
...
In [28]:
linits.size
Out[28]:
res27: Int = 164
In [29]:
linits.head.toString
Out[29]:
res28: String = "(P\u2080(InIsle((a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs,@a,Island(Typs,Typs,AddVar,Sigma,InIsle)))) == ((IsleScale(@a,(a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs)) * (P\u2080((a : M ) ~> (((eqM) (((mul) (e_l)) (a))) (a)) \u2208 Typs)))"
In [30]:
linits.head.rhs
Out[30]:
res29: Expression = Product(
  IsleScale(@a, Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
  InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs))
)
In [31]:
linits.head.lhs
Out[31]:
res30: Expression = InitialVal(
  InIsle(
    Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
    @a,
    Island(Typs, ConstRandVar(Typs), AddVar((M → (M → M)), 0.3), Sigma, InIsle)
  )
)
In [32]:
val termEqs = eqgs.collect{case Equation(FinalVal(Elem(t : Term, Terms)), rhs) => t -> rhs}
Out[32]:
termEqs: Set[(Term, Expression)] = Set(
  (
    (_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ eqM,
    Sum(
      Product(
        Product(
          Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
          FinalVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs))
        ),
        FinalVal(Elem((_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ eqM, Terms))
      ),
      Product(
        Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
        FinalVal(
          InIsle(
            Elem(eqM, Terms),
            @a,
            Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.3), Lambda, InIsle)
          )
        )
      )
    )
  ),
  (
    mul(e_r)(e_r),
    Sum(
      Product(
        Product(
          Coeff(FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms), Terms),
          FinalVal(Elem(Wrap(mul(e_r)), Funcs))
        ),
        FinalVal(Elem(e_r, AtCoord(TermsWithTyp, M :: HNil)))
      ),
      Product(
        Product(
          Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
          FinalVal(Elem(Wrap(mul(e_r)), Funcs))
        ),
        FinalVal(Elem(e_r, Terms))
      )
    )
  ),
  (
    axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_r)(e_r)(axiom_{eqM(a)(a)}(e_r)),
    Product(
      Product(
        Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
        FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs))
      ),
...
In [33]:
termEqs.size
Out[33]:
res32: Int = 127
In [34]:
termEqs.map(_._1)
Out[34]:
res33: Set[Term] = Set(
  axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_l)(axiom_{eqM(mul(a)(e_r))(a)}(e_l)),
  axiom_{(eqM(a)(b) \to eqM(b)(a))},
  mul(e_r)(e_l),
  eqM(e_r)(e_r),
  (_ : M) ↦ e_r,
  (_ : ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }) ↦ eqM,
  (_ : (M → (M → M))) ↦ axiom_{eqM(mul(e_l)(a))(a)},
  (_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ axiom_{eqM(mul(a)(e_r))(a)},
  (_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ e_l,
  (_ : ∏(a : M){ eqM(a)(a) }) ↦ mul,
  (_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ axiom_{eqM(mul(a)(e_r))(a)},
  (_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ e_l,
  eqM(e_r)(e_l),
  (_ : (M → (M → 𝒰 ))) ↦ axiom_{eqM(mul(a)(e_r))(a)},
  mul(e_r),
  axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
  (_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ mul,
  (@a : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ @a,
  (@a : (M → (M → 𝒰 ))) ↦ @a(e_r),
  (_ : (M → (M → 𝒰 ))) ↦ e_l,
  eqM(e_l)(e_l),
  (_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ axiom_{eqM(mul(e_l)(a))(a)},
  (_ : (M → (M → 𝒰 ))) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
  (_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ axiom_{eqM(mul(a)(e_r))(a)},
  (@a : (M → (M → 𝒰 ))) ↦ @a(e_l),
  (_ : ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
  (_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ axiom_{(eqM(a)(b) \to eqM(b)(a))},
  (_ : ∏(a : M){ eqM(a)(a) }) ↦ axiom_{eqM(a)(a)},
  axiom_{eqM(mul(a)(e_r))(a)}(e_r),
  axiom_{eqM(mul(e_l)(a))(a)},
  (_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ mul,
  mul,
  eqM(e_r),
  (@a : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ @a,
  (_ : ∏(a : M){ eqM(a)(a) }) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
  (_ : (M → (M → 𝒰 ))) ↦ eqM,
  axiom_{eqM(a)(a)}(e_r),
  (_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ eqM,
  ($tia : M) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(mul(e_l)(e_r))(e_l)($tia)(axiom_{eqM(mul(a)(e_r))(a)}(e_l)),
  (@a : M) ↦ @a,
  ($sxc : M) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_r)(e_r)($sxc)(axiom_{eqM(a)(a)}(e_r)),
  axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_l),
  (_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
...
In [35]:
termEqs.map(_._1.typ).filter(tp => !isUniv(tp))
Out[35]:
res34: Set[Typ[U] forSome { type U >: x$1._1.type <: Term with Subs[U]; val x$1: (Term, Expression) }] = Set(
  ∏($tcy : M){ (eqM(e_l)($tcy) → eqM(mul(e_l)(e_l))($tcy)) },
  eqM(e_r)(e_r),
  eqM(mul(e_l)(e_r))(e_l),
  (∏(a : M){ eqM(mul(e_l)(a))(a) } → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
  (∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } } → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
  (∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } } → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
  (∏(a : M){ eqM(a)(a) } → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
  (M → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
  (∏(a : M){ eqM(mul(a)(e_r))(a) } → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
  ((M → (M → M)) → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
  ((M → (M → 𝒰 )) → ∏(a : M){ eqM(mul(e_l)(a))(a) }),
  eqM(e_l)(e_l),
  ∏(a : M){ eqM(mul(e_l)(a))(a) },
  (∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } } → M),
  (M → M),
  (∏(a : M){ eqM(mul(a)(e_r))(a) } → M),
  (∏(a : M){ eqM(mul(e_l)(a))(a) } → M),
  (∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } } → M),
  (∏(a : M){ eqM(a)(a) } → M),
  ((M → (M → M)) → M),
  ((M → (M → 𝒰 )) → M),
  eqM(mul(e_l)(e_l))(e_l),
  ((M → (M → M)) → (M → (M → M))),
  (∏(a : M){ eqM(mul(a)(e_r))(a) } → (M → (M → M))),
  (M → (M → (M → M))),
  (∏(a : M){ eqM(a)(a) } → (M → (M → M))),
  ((M → (M → 𝒰 )) → (M → (M → M))),
  (∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } } → (M → (M → M))),
  (∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } } → (M → (M → M))),
  (∏(a : M){ eqM(mul(e_l)(a))(a) } → (M → (M → M))),
  (∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } } → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
  (∏(a : M){ eqM(mul(a)(e_r))(a) } → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
  (∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } } → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
  (∏(a : M){ eqM(a)(a) } → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
  ((M → (M → M)) → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
  ((M → (M → 𝒰 )) → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
  (M → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
  (∏(a : M){ eqM(mul(e_l)(a))(a) } → ∏(a : M){ eqM(mul(a)(e_r))(a) }),
  ∏($szu : M){ (eqM(e_r)($szu) → eqM(mul(e_l)(e_r))($szu)) },
  ∏($tia : M){ (eqM(e_l)($tia) → eqM(mul(e_l)(e_r))($tia)) },
  M,
  eqM(e_l)(mul(e_l)(e_r)),
  ((M → (M → M)) → (M → M)),
  (M → (M → M)),
  ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
...
In [36]:
val eqid = termEqs.find(_._1.typ == eqM(l)(op(l)(r)))
Out[36]:
eqid: Option[(Term, Expression)] = Some(
  (
    axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_l)(axiom_{eqM(mul(a)(e_r))(a)}(e_l)),
    Product(
      Product(
        Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
        FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs))
      ),
      FinalVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}(e_l), Terms))
    )
  )
)

This is a case of symmetry being applied, and presumably the equation is passed on too.

In [37]:
val eqid0 = termEqs.find(_._1.typ == eqM(op(l)(r))(l))
Out[37]:
eqid0: Option[(Term, Expression)] = Some(
  (
    axiom_{eqM(mul(a)(e_r))(a)}(e_l),
    Sum(
      Sum(
        Sum(
          Sum(
            Sum(
              Sum(
                Sum(
                  Sum(
                    Sum(
                      Sum(
                        Product(
                          Product(
                            Coeff(
                              BaseThenCondition(
                                ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms),
                                AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil),
                                Filter(WithTyp((M → (M → 𝒰 ))))
                              ),
                              AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil)
                            ),
                            FinalVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs))
                          ),
                          FinalVal(Elem(e_l, Terms))
                        ),
                        Product(
                          Product(
                            Coeff(
                              BaseThenCondition(
                                FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
                                AtCoord(TermsWithTyp, M :: HNil),
                                Filter(WithTyp(M))
                              ),
                              AtCoord(TermsWithTyp, M :: HNil)
                            ),
                            FinalVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs))
                          ),
                          FinalVal(Elem(e_l, AtCoord(TermsWithTyp, M :: HNil)))
                        )
                      ),
                      Product(
                        Product(
                          Coeff(
                            BaseThenCondition(
                              FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
                              Funcs,
                              Restrict(FuncOpt)
...
In [38]:
eqgs.find(eq => varVals(eq.rhs).intersect(extras).nonEmpty)
Out[38]:
res37: Option[Equation] = Some(
  Equation(
    InitialVal(
      InIsle(
        Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar((M → (M → M)), 0.3), Sigma, InIsle)
      )
    ),
    Product(
      IsleScale(@a, Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
      InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs))
    )
  )
)
In [39]:
val finExtras = extras -- initExtras
Out[39]:
finExtras: Set[VarVal[_]] = Set()
In [40]:
finExtras.size
Out[40]:
res39: Int = 0
In [41]:
val ats = eqs.map(_.rhs).flatMap(Expression.atoms)
Out[41]:
ats: Set[Expression] = Set(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  InitialVal(
    InIsle(
      Elem(e_l, Terms),
      @a,
      Island(
        AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
        ConstRandVar(Terms),
...
In [42]:
val coeffs = ats.collect{case coeff @ Coeff(_, _) => coeff}
Out[42]:
coeffs: Set[Coeff[Any]] = Set(
  Coeff(
    BaseThenCondition(
      ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms),
      AtCoord(TermsWithTyp, (M → (M → M)) :: HNil),
      Filter(WithTyp((M → (M → M))))
    ),
    AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)
  ),
  Coeff(
    BaseThenCondition(ZipMapOpt(UnifApplnOpt, TypFamilies, Terms, Terms), Typs, Restrict(TypOpt)),
    Typs
  ),
  Coeff(
    BaseThenCondition(
      FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
      AtCoord(TermsWithTyp, M :: HNil),
      Filter(WithTyp(M))
    ),
    AtCoord(TermsWithTyp, M :: HNil)
  ),
  Coeff(BaseThenCondition(FlatMap(Typs, LambdaIsle, Terms), Funcs, Restrict(FuncOpt)), Funcs),
  Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
  Coeff(
    FlatMap(Typs, provingground.learning.TermGeneratorNodes$$Lambda$2282/1458646167@3b664a79, Typs),
    Typs
  ),
  Coeff(
    Island(
      AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
      ConstRandVar(Terms),
      AddVar((M → (M → M)), 0.3),
      Lambda,
      InIsle
    ),
    AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
  ),
  Coeff(
    BaseThenCondition(
      FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
      Funcs,
      Restrict(FuncOpt)
    ),
    Funcs
  ),
  Coeff(
    Init(AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)),
    AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)
  ),
...
In [43]:
val cs =  coeffs.toVector.map(c => c.get(tg.nodeCoeffSeq) -> c.rv)
Out[43]:
cs: Vector[(Option[Double], RandomVar[Any])] = Vector(
  (Some(0.1), AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)),
  (Some(0.1), Typs),
  (Some(0.1), AtCoord(TermsWithTyp, M :: HNil)),
  (Some(0.1), Funcs),
  (Some(0.05), Terms),
  (Some(0.1), Typs),
  (Some(0.1), AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)),
  (Some(0.1), Funcs),
  (Some(0.16500000000000004), AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)),
  (Some(0.1), AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil)),
  (Some(0.30000000000000004), TargetTyps),
  (Some(0.1), AtCoord(TermsWithTyp, M :: HNil)),
  (Some(0.1), Terms),
  (Some(0.1), Terms),
  (Some(0.55), Terms),
  (Some(0.16500000000000004), AtCoord(TermsWithTyp, M :: HNil)),
  (Some(0.55), TypFamilies),
  (Some(0.1), Terms),
  (Some(0.1), AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil)),
  (Some(0.1), Typs),
  (Some(0.1), AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil)),
  (Some(0.55), AtCoord(FuncsWithDomain, M :: HNil)),
  (Some(0.1), Terms),
  (Some(0.1), AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)),
  (Some(0.1), Funcs),
  (Some(0.55), Funcs),
  (Some(0.6), Typs),
  (Some(0.16500000000000004), AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil)),
  (Some(0.05), Typs)
)
In [44]:
val initEls = extras.collect{case el @ InitialVal(Elem(_, _)) => el}
Out[44]:
initEls: Set[InitialVal[Any]] = Set(
  InitialVal(Elem(mul, Terms)),
  InitialVal(Elem(e_r, Terms)),
  InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)),
  InitialVal(
    Elem(
      Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}),
      AtCoord(FuncsWithDomain, M :: HNil)
    )
  ),
  InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(eqM, AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil))),
  InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), Funcs)),
  InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)),
  InitialVal(Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)),
  InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }, Typs)),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem((M → (M → M)), Typs)),
  InitialVal(Elem(eqM, Terms)),
  InitialVal(Elem(∏(a : M){ eqM(mul(a)(e_r))(a) }, Typs)),
  InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs)),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), Funcs)),
  InitialVal(Elem(Wrap(eqM), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, Typs)),
  InitialVal(Elem(M, Typs)),
  InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(Wrap(@a), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(Wrap(mul), Funcs)),
  InitialVal(Elem(Wrap(@a), Funcs)),
  InitialVal(Elem(axiom_{eqM(mul(e_l)(a))(a)}, Terms)),
  InitialVal(Elem(Wrap(mul), AtCoord(FuncsWithDomain, M :: HNil))),
  InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(∏(a : M){ eqM(a)(a) }, Typs)),
  InitialVal(Elem(e_r, AtCoord(TermsWithTyp, M :: HNil))),
  InitialVal(Elem(mul, AtCoord(TermsWithTyp, (M → (M → M)) :: HNil))),
  InitialVal(Elem((M → (M → 𝒰 )), Typs)),
  InitialVal(Elem(e_l, AtCoord(TermsWithTyp, M :: HNil))),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)),
...
In [45]:
extras -- initEls
Out[45]:
res44: Set[VarVal[_]] = Set()
In [46]:
val sd = implicitly[StateDistribution[TermState, FiniteDistribution]]
Out[46]:
sd: StateDistribution[TermState, FiniteDistribution] = provingground.learning.TermState$$anon$1@5311ab99
In [47]:
val zeroVals =  initEls.filter{case InitialVal(Elem(x, rv)) => sd.value(ts)(rv)(x) == 0}
Out[47]:
zeroVals: Set[InitialVal[Any]] = Set(
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(Wrap(@a), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(Wrap(@a), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms))
)
In [48]:
val withZero = eqs.filter(eq => varVals(eq.rhs).intersect(zeroVals.map(x => x : VarVal[_])).nonEmpty)
Out[48]:
withZero: Set[EquationTerm] = Set(
  EquationTerm(
    InitialVal(
      InIsle(
        Elem(@a, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
      )
    ),
    Product(IsleScale(@a, Elem(@a, Terms)), InitialVal(Elem(@a, Terms)))
  ),
  EquationTerm(
    InitialVal(
      InIsle(Elem(@a, Terms), @a, Island(Terms, ConstRandVar(Terms), AddVar(M, 0.3), Lambda, InIsle))
    ),
    Product(IsleScale(@a, Elem(@a, Terms)), InitialVal(Elem(@a, Terms)))
  ),
  EquationTerm(
    InitialVal(
      InIsle(
        Elem(@a, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar((M → (M → 𝒰 )), 0.3), Lambda, InIsle)
      )
    ),
    Product(IsleScale(@a, Elem(@a, Terms)), InitialVal(Elem(@a, Terms)))
  ),
  EquationTerm(
    InitialVal(
      InIsle(
        Elem(@a, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.3), Lambda, InIsle)
      )
    ),
    Product(IsleScale(@a, Elem(@a, Terms)), InitialVal(Elem(@a, Terms)))
  ),
  EquationTerm(
    InitialVal(
      InIsle(
        Elem(@a, Terms),
        @a,
        Island(
          AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
          ConstRandVar(Terms),
          AddVar((M → (M → 𝒰 )), 0.3),
          Lambda,
          InIsle
        )
...
In [49]:
val atoms = ats.union(lefts)
Out[49]:
atoms: Set[Expression] = Set(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  FinalVal(
    Elem(
      ((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ),
  FinalVal(
...
In [50]:
import ExpressionEval._
Out[50]:
import ExpressionEval._
In [51]:
val init = initMap(atoms, tg, ts)
Out[51]:
init: Map[Expression, Double] = Map(
  IsleScale(@a, Elem(mul, Terms)) -> 0.7,
  InitialVal(Elem(mul, Terms)) -> 0.3333333333333333,
  InitialVal(Elem(e_r, Terms)) -> 0.047619047619047616,
  IsleScale(@a, Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), Funcs)) -> 0.7,
  Coeff(
    BaseThenCondition(
      ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms),
      AtCoord(TermsWithTyp, (M → (M → M)) :: HNil),
      Filter(WithTyp((M → (M → M))))
    ),
    AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)
  ) -> 0.1,
  Coeff(
    BaseThenCondition(ZipMapOpt(UnifApplnOpt, TypFamilies, Terms, Terms), Typs, Restrict(TypOpt)),
    Typs
  ) -> 0.1,
  InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)) -> 0.047619047619047616,
  InitialVal(
    Elem(
      Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}),
      AtCoord(FuncsWithDomain, M :: HNil)
    )
  ) -> 0.052631578947368425,
  IsleScale(@a, Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)) -> 0.7,
  InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)) -> 0.047619047619047616,
  Coeff(
    BaseThenCondition(
      FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
      AtCoord(TermsWithTyp, M :: HNil),
      Filter(WithTyp(M))
    ),
    AtCoord(TermsWithTyp, M :: HNil)
  ) -> 0.1,
  Coeff(BaseThenCondition(FlatMap(Typs, LambdaIsle, Terms), Funcs, Restrict(FuncOpt)), Funcs) -> 0.1,
  IsleScale(@a, Elem(e_l, Terms)) -> 0.7,
  IsleScale(@a, Elem(eqM, Terms)) -> 0.7,
  IsleScale(@a, Elem(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, Typs)) -> 0.7,
  IsleScale(@a, Elem(∏(a : M){ eqM(mul(e_l)(a))(a) }, Typs)) -> 0.7,
  IsleScale(@a, Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)) -> 0.7,
  InitialVal(Elem(Wrap(axiom_{eqM(mul(e_l)(a))(a)}), AtCoord(FuncsWithDomain, M :: HNil))) -> 0.052631578947368425,
  IsleScale(@a, Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)) -> 0.7,
  InitialVal(Elem(eqM, AtCoord(TermsWithTyp, (M → (M → 𝒰 )) :: HNil))) -> 1.0,
  IsleScale(@a, Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)) -> 0.7,
  InitialVal(Elem(Wrap(axiom_{eqM(a)(a)}), Funcs)) -> 0.05263157894736841,
  InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)) -> 0.047619047619047616,
...
In [52]:
init.size
Out[52]:
res51: Int = 187
In [53]:
val m2 = nextMap(init, eqgs)
Out[53]:
m2: Map[Expression, Double] = Map(
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.036842105263157884,
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.033333333333333326,
  InitialVal(
    InIsle(
      Elem(e_l, Terms),
      @a,
      Island(
        AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
        ConstRandVar(Terms),
        AddVar((M → (M → 𝒰 )), 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.033333333333333326,
  IsleScale(@a, Elem(mul, Terms)) -> 0.7,
  InitialVal(Elem(mul, Terms)) -> 0.3333333333333333,
  FinalVal(Elem(mul, Terms)) -> 0.18333333333333335,
  InitialVal(
    InIsle(
      Elem(Wrap(@a), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.3,
  InitialVal(
    InIsle(
      Elem(e_r, Terms),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(a)(a) }, 0.3), Lambda, InIsle)
...
In [54]:
m2.size
Out[54]:
res53: Int = 387
In [55]:
val m3 = nextMap(m2, eqgs)
Out[55]:
m3: Map[Expression, Double] = Map(
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.036842105263157884,
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.020263157894736837,
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.01833333333333333,
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.033333333333333326,
  FinalVal(
    InIsle(
      Elem(e_l, Terms),
      @a,
      Island(
        AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil),
        ConstRandVar(Terms),
        AddVar((M → (M → 𝒰 )), 0.3),
...
In [56]:
m3.size
Out[56]:
res55: Int = 573
In [57]:
atoms.size
Out[57]:
res56: Int = 772
In [58]:
atoms -- m3.keys
Out[58]:
res57: Set[Expression] = Set(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)),
  FinalVal(
    Elem(
      ((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ),
  FinalVal(
    Elem(
      ((M → (M → M)) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ),
  FinalVal(
    Elem(
      ($stt : M) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(mul(e_r)(e_r))(e_r)($stt)(axiom_{eqM(mul(a)(e_r))(a)}(e_r)),
      Terms
    )
  ),
  FinalVal(Elem((_ : ∏(a : M){ eqM(a)(a) }) ↦ axiom_{eqM(mul(e_l)(a))(a)}, Terms)),
  FinalVal(Elem((_ : (M → (M → M))) ↦ axiom_{eqM(mul(e_l)(a))(a)}, Terms)),
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(e_l)(a))(a)}(e_l), Terms),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ),
  FinalVal(
    Elem(Wrap((_ : (M → (M → 𝒰 ))) ↦ e_r), AtCoord(FuncsWithDomain, (M → (M → 𝒰 )) :: HNil))
  ),
  FinalVal(
    InIsle(
      Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_r), Terms),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → 𝒰 )), 0.3), Lambda, InIsle)
    )
  ),
  FinalVal(Elem((_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ mul, Terms)),
  FinalVal(Elem((M → (M → 𝒰 ))×(M → (M → M)), Typs)),
  FinalVal(Elem((_ : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)),
  FinalVal(Elem((_ : M) ↦ e_r, Terms)),
  FinalVal(
    Elem((_ : ∏(a : M){ eqM(a)(a) }) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)
  ),
  FinalVal(
    Elem(
...
In [59]:
m2.values.toSet
Out[59]:
res58: Set[Double] = Set(
  0.057142857142857134,
  0.028947368421052635,
  0.16500000000000004,
  0.3,
  0.6,
  0.028571428571428567,
  1.0,
  0.09523809523809523,
  0.033333333333333326,
  0.06666666666666665,
  0.052631578947368425,
  0.047619047619047616,
  0.3333333333333333,
  0.08250000000000002,
  0.7,
  0.05,
  0.1,
  0.5,
  0.18333333333333335,
  0.36842105263157887,
  0.19999999999999998,
  0.55,
  0.028947368421052628,
  0.05263157894736841,
  0.20263157894736838,
  0.2578947368421052,
  0.036842105263157884,
  0.2333333333333333,
  0.4285714285714286,
  0.3684210526315789,
  0.2026315789473684,
  0.02619047619047619,
  0.30000000000000004
)
In [60]:
init.filter(_._1.isInstanceOf[Coeff[_]])
Out[60]:
res59: Map[Expression, Double] = Map(
  Coeff(
    BaseThenCondition(
      ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms),
      AtCoord(TermsWithTyp, (M → (M → M)) :: HNil),
      Filter(WithTyp((M → (M → M))))
    ),
    AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)
  ) -> 0.1,
  Coeff(
    BaseThenCondition(ZipMapOpt(UnifApplnOpt, TypFamilies, Terms, Terms), Typs, Restrict(TypOpt)),
    Typs
  ) -> 0.1,
  Coeff(
    BaseThenCondition(
      FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
      AtCoord(TermsWithTyp, M :: HNil),
      Filter(WithTyp(M))
    ),
    AtCoord(TermsWithTyp, M :: HNil)
  ) -> 0.1,
  Coeff(BaseThenCondition(FlatMap(Typs, LambdaIsle, Terms), Funcs, Restrict(FuncOpt)), Funcs) -> 0.1,
  Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms) -> 0.05,
  Coeff(
    FlatMap(Typs, provingground.learning.TermGeneratorNodes$$Lambda$2282/1458646167@3b664a79, Typs),
    Typs
  ) -> 0.1,
  Coeff(
    Island(
      AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil),
      ConstRandVar(Terms),
      AddVar((M → (M → M)), 0.3),
      Lambda,
      InIsle
    ),
    AtCoord(FuncsWithDomain, (M → (M → M)) :: HNil)
  ) -> 0.1,
  Coeff(
    BaseThenCondition(
      FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
      Funcs,
      Restrict(FuncOpt)
    ),
    Funcs
  ) -> 0.1,
  Coeff(
    Init(AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)),
    AtCoord(TermsWithTyp, (M → (M → M)) :: HNil)
...
In [61]:
val m4 = nextMap(m3, eqgs)
Out[61]:
m4: Map[Expression, Double] = Map(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.0165,
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.036842105263157884,
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.020263157894736837,
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.01833333333333333,
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.033333333333333326,
  FinalVal(
    Elem(
      ((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ) -> 0.0019999999999999996,
  FinalVal(
...
In [62]:
m4.size
Out[62]:
res61: Int = 757
In [63]:
val m5 = nextMap(m4, eqgs)
Out[63]:
m5: Map[Expression, Double] = Map(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.01652355461584635,
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.036842105263157884,
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.020263157894736837,
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.01833333333333333,
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.033333333333333326,
  FinalVal(
    Elem(
      ((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ) -> 0.0019999999999999996,
  FinalVal(
...
In [64]:
m5.size
Out[64]:
res63: Int = 768
In [65]:
atoms -- m5.keySet
Out[65]:
res64: Set[Expression] = Set(
  FinalVal(Elem((@a : (M → (M → M))) ↦ @a(e_r), Terms)),
  FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a(e_r), Terms)),
  FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a(e_l), Terms)),
  FinalVal(Elem((@a : (M → (M → M))) ↦ @a(e_l), Terms))
)
In [66]:
val zeroE = eqgs.filter(eq => !m5.keySet(eq.lhs))
Out[66]:
zeroE: Set[Equation] = Set(
  Equation(
    FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a(e_l), Terms)),
    Product(
      Product(
        Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
        FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs))
      ),
      FinalVal(Elem(e_l, Terms))
    )
  ),
  Equation(
    FinalVal(Elem((@a : (M → (M → M))) ↦ @a(e_l), Terms)),
    Product(
      Product(
        Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
        FinalVal(Elem(Wrap((@a : (M → (M → M))) ↦ @a), Funcs))
      ),
      FinalVal(Elem(e_l, Terms))
    )
  ),
  Equation(
    FinalVal(Elem((@a : (M → (M → M))) ↦ @a(e_r), Terms)),
    Product(
      Product(
        Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
        FinalVal(Elem(Wrap((@a : (M → (M → M))) ↦ @a), Funcs))
      ),
      FinalVal(Elem(e_r, Terms))
    )
  ),
  Equation(
    FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a(e_r), Terms)),
    Product(
      Product(
        Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
        FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs))
      ),
      FinalVal(Elem(e_r, Terms))
    )
  )
)
In [67]:
zeroE.head.rhs
Out[67]:
res66: Expression = Product(
  Product(
    Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
    FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs))
  ),
  FinalVal(Elem(e_l, Terms))
)
In [68]:
val x = Expression.atoms(zeroE.head.rhs).filter(exp => recExp(m4, exp) == 0).head
Out[68]:
x: Expression = FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs))
In [69]:
eqgs.find(_.lhs == x)
Out[69]:
res68: Option[Equation] = Some(
  Equation(
    FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs)),
    Quotient(
      FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a, Terms)),
      FinalVal(Event(Terms, Restrict(FuncOpt)))
    )
  )
)
In [70]:
val ts = Expression.atoms(eqgs.find(_.lhs == x).get.rhs).toVector
Out[70]:
ts: Vector[Expression] = Vector(
  FinalVal(Elem((@a : (M → (M → 𝒰 ))) ↦ @a, Terms)),
  FinalVal(Event(Terms, Restrict(FuncOpt)))
)
In [71]:
ts.map(m4.get(_))
Out[71]:
res70: Vector[Option[Double]] = Vector(Some(0.033), None)
In [72]:
val eventEq = eqgs.find(_.lhs == ts(1)).get
Out[72]:
eventEq: Equation = Equation(
  FinalVal(Event(Terms, Restrict(FuncOpt))),
  Sum(
    Sum(
      Sum(
        Sum(
          Sum(
            Sum(
              Sum(
                Sum(
                  Sum(
                    FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_r)), Funcs)),
                    FinalVal(Elem(Wrap(eqM(e_l)), Funcs))
                  ),
                  FinalVal(Elem(Wrap(eqM(e_r)), Funcs))
                ),
                FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_r)), Funcs))
              ),
              FinalVal(Elem(Wrap(mul(e_l)), Funcs))
            ),
            FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_l)), Funcs))
          ),
          FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_l)), Funcs))
        ),
        FinalVal(Elem(Wrap(mul(e_r)), Funcs))
      ),
      Sum(
        FinalVal(Elem(Wrap((@a : (M → (M → M))) ↦ @a), Funcs)),
        FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs))
      )
    ),
    Sum(
      Sum(
        Sum(FinalVal(Elem(Wrap(mul(e_l)), Funcs)), FinalVal(Elem(Wrap(eqM(e_l)), Funcs))),
        FinalVal(Elem(Wrap(mul(e_r)), Funcs))
      ),
      FinalVal(Elem(Wrap(eqM(e_r)), Funcs))
    )
  )
)
In [73]:
val m6 = nextMap(m5, eqgs)
Out[73]:
m6: Map[Expression, Double] = Map(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.016535378155739335,
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.036842105263157884,
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.020263157894736837,
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.01833333333333333,
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.033333333333333326,
  FinalVal(
    Elem(
      ((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ) -> 0.0019999999999999996,
  FinalVal(
...
In [74]:
m6.size
Out[74]:
res73: Int = 772
In [75]:
atoms -- m6.keySet
Out[75]:
res74: Set[Expression] = Set()
In [76]:
val ms = stableSupportMap(init, eqgs)
Out[76]:
ms: Map[Expression, Double] = Map(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.016541309982685166,
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.036842105263157884,
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.020263157894736837,
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.01833333333333333,
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.033333333333333326,
  FinalVal(
    Elem(
      ((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ) -> 0.0019999999999999996,
  FinalVal(
...
In [77]:
val m100 = iterateMap(ms, eqgs, 100)
Out[77]:
m100: Map[Expression, Double] = Map(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.016547277936962753,
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.036842105263157884,
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.020263157894736837,
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.01833333333333333,
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.033333333333333326,
  FinalVal(
    Elem(
      ((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ) -> 0.0019999999999999996,
  FinalVal(
...
In [78]:
val m200 = iterateMap(m100, eqgs, 100)
Out[78]:
m200: Map[Expression, Double] = Map(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> 0.016547277936962753,
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.036842105263157884,
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 0.020263157894736837,
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.01833333333333333,
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> 0.033333333333333326,
  FinalVal(
    Elem(
      ((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ) -> 0.0019999999999999996,
  FinalVal(
...
In [79]:
mapRatio(m100, m200)
Out[79]:
res78: Double = 1.0000000000000009
In [80]:
mapRatio(ms, m100)
Out[80]:
res79: Double = 2.0112732240884026
In [81]:
zeroVals
Out[81]:
res80: Set[InitialVal[Any]] = Set(
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(Wrap(@a), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(Wrap(@a), Funcs)),
  InitialVal(Elem(@a, Terms)),
  InitialVal(Elem(@a, Terms))
)
In [82]:
zeroVals.map{case InitialVal(elem : Elem[_]) => isIsleVar(elem)}
Out[82]:
res81: Set[Boolean] = Set(true)
In [83]:
val ins = TermState(dist1, dist1.map(_.typ))
val fsT = tg.nextStateTask(ins, 0.001)
val fs = fsT.runSyncUnsafe()
Out[83]:
ins: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(e_l, 0.047619047619047616),
      Weighted(e_r, 0.047619047619047616),
      Weighted(mul, 0.047619047619047616),
      Weighted(eqM, 0.047619047619047616),
      Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
      Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.047619047619047616),
      Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
      Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
      Weighted(eqM, 0.2857142857142857),
      Weighted(mul, 0.2857142857142857)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.047619047619047616),
      Weighted(M, 0.047619047619047616),
      Weighted((M → (M → M)), 0.047619047619047616),
      Weighted((M → (M → 𝒰 )), 0.047619047619047616),
      Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
      Weighted(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.047619047619047616),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.047619047619047616
      ),
      Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
      Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
      Weighted((M → (M → 𝒰 )), 0.2857142857142857),
      Weighted((M → (M → M)), 0.2857142857142857)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
fsT: monix.eval.Task[TermState] = FlatMap(
  FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$2530/1333989368@2030de41),
  provingground.learning.TermGenParams$$Lambda$3341/1899735046@45f00ab8
)
fs: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.029778252577854582),
      Weighted(mul(e_r)(e_l), 0.0053934227946860315),
      Weighted(eqM(e_r)(e_r), 0.0053934227946860315),
      Weighted((_ : ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }) ↦ eqM, 0.0011761943024481748),
      Weighted((_ : (M → (M → M))) ↦ axiom_{eqM(mul(e_l)(a))(a)}, 0.0011761943024481746),
      Weighted((_ : ∏(a : M){ eqM(a)(a) }) ↦ mul, 0.0011761943024481748),
      Weighted(eqM(e_r)(e_l), 0.0053934227946860315),
      Weighted((_ : (M → (M → 𝒰 ))) ↦ axiom_{eqM(mul(a)(e_r))(a)}, 0.0011761943024481746),
      Weighted(mul(e_r), 0.02478994011666693),
      Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.029778252577854582),
      Weighted((_ : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ mul, 0.0011761943024481748),
      Weighted((@a : ∏(a : M){ eqM(mul(e_l)(a))(a) }) ↦ @a, 0.0015122498174333678),
      Weighted((@a : (M → (M → 𝒰 ))) ↦ @a(e_r), 0.0023589908047798197),
      Weighted((_ : (M → (M → 𝒰 ))) ↦ e_l, 0.0011761943024481746),
      Weighted(eqM(e_l)(e_l), 0.0053934227946860315),
      Weighted(
        (_ : (M → (M → 𝒰 ))) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.0011761943024481746
      ),
      Weighted((@a : (M → (M → 𝒰 ))) ↦ @a(e_l), 0.0023589908047798197),
      Weighted(axiom_{eqM(mul(a)(e_r))(a)}(e_r), 0.003541420016666704),
      Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.029778252577854582),
      Weighted(
        (_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ mul,
        0.0011761943024481748
      ),
      Weighted(mul, 0.24983231236562614),
      Weighted(eqM(e_r), 0.02478994011666693),
      Weighted(
        (@a : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ @a,
        0.0015122498174333675
      ),
      Weighted((_ : (M → (M → 𝒰 ))) ↦ eqM, 0.008233360117137222),
      Weighted(axiom_{eqM(a)(a)}(e_r), 0.003541420016666704),
      Weighted(
        (_ : ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }) ↦ eqM,
        0.0011761943024481748
      ),
      Weighted((@a : M) ↦ @a, 0.0030244996348667355),
      Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_l), 0.003541420016666704),
      Weighted((@a : (M → (M → 𝒰 ))) ↦ @a, 0.010585748722033573),
      Weighted((@a : ∏(a : M){ eqM(a)(a) }) ↦ @a, 0.0015122498174333678),
      Weighted((_ : (M → (M → M))) ↦ axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.0011761943024481746),
      Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.029778252577854582),
      Weighted(e_l, 0.033331339533166776),
      Weighted(axiom_{eqM(a)(a)}, 0.029778252577854582),
...
In [84]:
val expEv = ExpressionEval.fromStates(ins, fs, eqgs, tg)
Out[84]:
expEv: ExpressionEval = ExpressionEval(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(e_l, 0.047619047619047616),
        Weighted(e_r, 0.047619047619047616),
        Weighted(mul, 0.047619047619047616),
        Weighted(eqM, 0.047619047619047616),
        Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
        Weighted(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, 0.047619047619047616),
        Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
        Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
        Weighted(eqM, 0.2857142857142857),
        Weighted(mul, 0.2857142857142857)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.047619047619047616),
        Weighted(M, 0.047619047619047616),
        Weighted((M → (M → M)), 0.047619047619047616),
        Weighted((M → (M → 𝒰 )), 0.047619047619047616),
        Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
        Weighted(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.047619047619047616),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.047619047619047616
        ),
        Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
        Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
        Weighted((M → (M → 𝒰 )), 0.2857142857142857),
        Weighted((M → (M → M)), 0.2857142857142857)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.029778252577854582),
        Weighted(mul(e_r)(e_l), 0.0053934227946860315),
        Weighted(eqM(e_r)(e_r), 0.0053934227946860315),
        Weighted((_ : ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }) ↦ eqM, 0.0011761943024481748),
        Weighted((_ : (M → (M → M))) ↦ axiom_{eqM(mul(e_l)(a))(a)}, 0.0011761943024481746),
...
In [85]:
expEv.hExp
Out[85]:
res84: Expression = Sum(
  Sum(
    Sum(
      Sum(
        Sum(
          Sum(
            Sum(
              Sum(
                Product(
                  Product(InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)), Literal(-1.0)),
                  Log(InitialVal(Elem(axiom_{(eqM(a)(b) \to eqM(b)(a))}, Terms)))
                ),
                Product(
                  Product(
                    InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)),
                    Literal(-1.0)
                  ),
                  Log(InitialVal(Elem(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}, Terms)))
                )
              ),
              Product(
                Product(InitialVal(Elem(axiom_{eqM(mul(e_l)(a))(a)}, Terms)), Literal(-1.0)),
                Log(InitialVal(Elem(axiom_{eqM(mul(e_l)(a))(a)}, Terms)))
              )
            ),
            Product(
              Product(InitialVal(Elem(mul, Terms)), Literal(-1.0)),
              Log(InitialVal(Elem(mul, Terms)))
            )
          ),
          Product(
            Product(InitialVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)), Literal(-1.0)),
            Log(InitialVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms)))
          )
        ),
        Product(
          Product(InitialVal(Elem(e_l, Terms)), Literal(-1.0)),
          Log(InitialVal(Elem(e_l, Terms)))
        )
      ),
      Product(
        Product(InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)), Literal(-1.0)),
        Log(InitialVal(Elem(axiom_{eqM(a)(a)}, Terms)))
      )
    ),
    Product(Product(InitialVal(Elem(eqM, Terms)), Literal(-1.0)), Log(InitialVal(Elem(eqM, Terms))))
  ),
  Product(Product(InitialVal(Elem(e_r, Terms)), Literal(-1.0)), Log(InitialVal(Elem(e_r, Terms))))
)
In [86]:
val v = expEv.entropyProjection()(m200)
Out[86]:
v: Vector[Double] = Vector(
  -4.9763786428984865E-8,
  4.304068722953969E-4,
  7.825579496279935E-4,
  -0.007865854590058665,
  -0.0043262200245322785,
  -6.6252189744191E-8,
  -6.625218974419076E-8,
  -7.330142310666104E-5,
  -0.0038753621373031275,
  -0.007046112976914767,
  -4.326220024532279E-4,
  -9.225422040748262E-4,
  -1.8508707244961254E-4,
  -3.875362137303129E-4,
  -0.01104766870010009,
  -0.01935346292461547,
  1.7524021516971672E-6,
  3.1861857303584815E-6,
  -0.007046112976914766,
  -0.003875362137303117,
  -1.7822492002662562E-4,
  -7.843743637793382E-4,
  -7.819762275242176E-6,
  -0.005535136690582533,
  -0.010065875681306813,
  -4.3262200245322737E-4,
  -3.875362137303143E-4,
  -4.3262200245322764E-4,
  -8.184021850128861E-5,
  -0.0061803143207604045,
  -0.011236935128655237,
  -7.843743637793366E-4,
  -0.004326220024532275,
  -0.007865854590058684,
  1.2054336828801602E-4,
  2.1916976052367254E-4,
  4.739556688640917E-10,
  8.61737579752899E-10,
  -0.004326220024532278,
  -0.007865854590058676,
  -3.46170946598965E-4,
  -0.007865854590058667,
  -0.004326220024532272,
  -0.003196253246208674,
  -0.001357545744697577,
  -0.002468264990359229,
  -9.225422040748282E-4,
  -6.625218974419083E-7,
...
In [87]:
val grad = expEv.variableIndex.mapValues(j => v(j))
Out[87]:
grad: Map[Expression, Double] = Map(
  FinalVal(Elem((@a : ∏(a : M){ eqM(mul(a)(e_r))(a) }) ↦ @a, Terms)) -> -4.9763786428984865E-8,
  FinalVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 4.304068722953969E-4,
  InitialVal(
    InIsle(
      Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
    )
  ) -> 7.825579496279935E-4,
  InitialVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> -0.007865854590058665,
  FinalVal(
    InIsle(
      Elem(axiom_{eqM(mul(a)(e_r))(a)}, Terms),
      @a,
      Island(
        Terms,
        ConstRandVar(Terms),
        AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
        Lambda,
        InIsle
      )
    )
  ) -> -0.0043262200245322785,
  FinalVal(
    Elem(
      ((M → (M → 𝒰 )) → ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } }),
      Typs
    )
  ) -> -6.6252189744191E-8,
  FinalVal(
...
In [88]:
grad.toVector.sortBy{case (_, p) => - math.abs(p)}
Out[88]:
res87: Vector[(Expression, Double)] = Vector(
  (InitialVal(Elem(eqM, Terms)), -0.019353462924615473),
  (InitialVal(Elem(mul, Terms)), -0.01935346292461547),
  (
    InitialVal(
      InIsle(Elem(eqM, Terms), @a, Island(Terms, ConstRandVar(Terms), AddVar(M, 0.3), Lambda, InIsle))
    ),
    -0.013547424047230871
  ),
  (
    InitialVal(
      InIsle(
        Elem(mul, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.3), Lambda, InIsle)
      )
    ),
    -0.013547424047230843
  ),
  (
    InitialVal(
      InIsle(
        Elem(mul, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(a)(a) }, 0.3), Lambda, InIsle)
      )
    ),
    -0.013547424047230833
  ),
  (
    InitialVal(
      InIsle(
        Elem(mul, Terms),
        @a,
        Island(
          Terms,
          ConstRandVar(Terms),
          AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
          Lambda,
          InIsle
        )
      )
    ),
    -0.013547424047230833
  ),
  (
    InitialVal(
      InIsle(
        Elem(eqM, Terms),
...
In [89]:
expEv.jet(m200)(expEv.hExp)
Out[89]:
res88: spire.math.Jet[Double] = Jet(
  3.119162312519754,
  Array(
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.07671320486001368,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.07671320486001368,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.07671320486001368,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
    -0.0,
...
In [90]:
expEv.jet(m200)(expEv.klExp)
Out[90]:
res89: spire.math.Jet[Double] = Jet(
  -1.9624979394717363,
  Array(
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    -9.191501396401179E-4,
    0.0,
    0.0,
    -0.12439165223129593,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    -9.191501396401179E-4,
    0.0,
    -0.005923412011014092,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    -0.017770236033042276,
    0.0,
    -9.191501396401179E-4,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    -0.018838158871566455,
    0.0,
    0.0,
...
In [91]:
import spire.algebra._
import spire.implicits._
v.norm
Out[91]:
import spire.algebra._

import spire.implicits._

res90_2: Double = 0.1112345315327967
In [92]:
val vv = expEv.entropyProjection()(expEv.finalDist)
Out[92]:
vv: Vector[Double] = Vector(
  -4.9763786428984865E-8,
  4.304068722953969E-4,
  7.825579496279935E-4,
  -0.007865854590058665,
  -0.0043262200245322785,
  -6.6252189744191E-8,
  -6.625218974419076E-8,
  -7.330142310666104E-5,
  -0.0038753621373031275,
  -0.007046112976914767,
  -4.326220024532279E-4,
  -9.225422040748262E-4,
  -1.8508707244961254E-4,
  -3.875362137303129E-4,
  -0.01104766870010009,
  -0.01935346292461547,
  1.7524021516971672E-6,
  3.1861857303584815E-6,
  -0.007046112976914766,
  -0.003875362137303117,
  -1.7822492002662562E-4,
  -7.843743637793382E-4,
  -7.819762275242176E-6,
  -0.005535136690582533,
  -0.010065875681306813,
  -4.3262200245322737E-4,
  -3.875362137303143E-4,
  -4.3262200245322764E-4,
  -8.184021850128861E-5,
  -0.0061803143207604045,
  -0.011236935128655237,
  -7.843743637793366E-4,
  -0.004326220024532275,
  -0.007865854590058684,
  1.2054336828801602E-4,
  2.1916976052367254E-4,
  4.739556688640917E-10,
  8.61737579752899E-10,
  -0.004326220024532278,
  -0.007865854590058676,
  -3.46170946598965E-4,
  -0.007865854590058667,
  -0.004326220024532272,
  -0.003196253246208674,
  -0.001357545744697577,
  -0.002468264990359229,
  -9.225422040748282E-4,
  -6.625218974419083E-7,
...
In [93]:
vv.norm
Out[93]:
res92: Double = 0.1112345315327967
In [94]:
val best = expEv.vars.zipWithIndex.sortBy{case (v, n) => -vv(n)}.map{case (v, n) => (v, vv(n))}
Out[94]:
best: Vector[(Expression, Double)] = Vector(
  (FinalVal(Elem(Wrap((@a : (M → (M → M))) ↦ @a), Funcs)), 0.0030554265290708275),
  (FinalVal(Elem(Wrap((@a : (M → (M → 𝒰 ))) ↦ @a), Funcs)), 0.0030554265290708062),
  (InitialVal(Elem(Wrap(eqM), Funcs)), 0.0016881778689094718),
  (
    InitialVal(
      InIsle(
        Elem(Wrap(eqM), Funcs),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
      )
    ),
    0.0011817245082366306
  ),
  (
    InitialVal(
      InIsle(
        Elem(Wrap(eqM), Funcs),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar((M → (M → 𝒰 )), 0.3), Lambda, InIsle)
      )
    ),
    0.001181724508236628
  ),
  (
    InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs)),
    0.0011179399280399904
  ),
  (InitialVal(Elem(Wrap(mul), Funcs)), 0.0011032460029815274),
  (FinalVal(Elem(Wrap(eqM), Funcs)), 9.284978279002059E-4),
  (InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)), 8.074382773262631E-4),
  (
    InitialVal(
      InIsle(
        Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar((M → (M → 𝒰 )), 0.3), Lambda, InIsle)
      )
    ),
    7.825579496279936E-4
  ),
  (
    InitialVal(
      InIsle(
        Elem(Wrap(axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}), Funcs),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar((M → (M → M)), 0.3), Lambda, InIsle)
      )
    ),
...
In [95]:
best.reverse
Out[95]:
res94: Vector[(Expression, Double)] = Vector(
  (InitialVal(Elem(eqM, Terms)), -0.019353462924615473),
  (InitialVal(Elem(mul, Terms)), -0.01935346292461547),
  (
    InitialVal(
      InIsle(Elem(eqM, Terms), @a, Island(Terms, ConstRandVar(Terms), AddVar(M, 0.3), Lambda, InIsle))
    ),
    -0.013547424047230871
  ),
  (
    InitialVal(
      InIsle(
        Elem(mul, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.3), Lambda, InIsle)
      )
    ),
    -0.013547424047230843
  ),
  (
    InitialVal(
      InIsle(
        Elem(eqM, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar((M → (M → 𝒰 )), 0.3), Lambda, InIsle)
      )
    ),
    -0.013547424047230833
  ),
  (
    InitialVal(
      InIsle(
        Elem(eqM, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.3), Lambda, InIsle)
      )
    ),
    -0.013547424047230833
  ),
  (
    InitialVal(
      InIsle(
        Elem(mul, Terms),
        @a,
        Island(
          Terms,
          ConstRandVar(Terms),
          AddVar(∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } }, 0.3),
          Lambda,
...
In [ ]: