Testing export and normalization of isles

This is a simplified version, by raising cutoffs and sharpening decays.

When we have variables such as $A: Type$, $a : A$ and $B: Type$, we test whether we correctly:

  • export equations, so that variables end up in islands
  • normalize isle names.

This time the test is more refined. Namely,

  • We generate with the equations after exporting and just $Type$ as the initial distribution.
  • We check that all terms are independent of the variables.
  • Generate with equations after normalization.
  • Make the same tests.
  • Also test if the distribution after normalization is approximately the same as before.

In [1]:
import $cp.bin.`provingground-core-jvm-b17f79ea57.fat.jar`
import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}


Out[1]:
import $cp.$                                              

import provingground._ , interface._, HoTT._, learning._ 

In [2]:
val A = "A" :: Type
val B = "B" :: Type
val a = "a" :: A
val ts = TermState(FiniteDistribution.unif(a), FiniteDistribution.unif(A, B), vars = Vector(A, B, a), context = Context.Empty.addVariable(A).addVariable(B).addVariable(a))


Out[2]:
A: Typ[Term] = A
B: Typ[Term] = B
a: Term = a
ts: TermState = TermState(
  FiniteDistribution(Vector(Weighted(a, 1.0))),
  FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
  Vector(A, B, a),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  AppendVariable(AppendVariable(AppendVariable(Empty, A), B), a)
)

In [3]:
val lp = LocalProver(ts)


Out[3]:
lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(Vector(Weighted(a, 1.0))),
    FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
    Vector(A, B, a),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    AppendVariable(AppendVariable(AppendVariable(Empty, A), B), a)
  ),
  TermGenParams(
    0.1,
    0.1,
    0.1,
    0.1,
    0.1,
    0.05,
    0.05,
    0.05,
    0.0,
    0.0,
    0.0,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.0,
    0.0,
    OrElse(
      OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
      <function1>
    )
  ),
  1.0E-4,
  None,
  12 minutes,
  1.01,
  1.0,
...

In [4]:
ts.vars
import TermData._
val datT = termData(lp)


Out[4]:
res3_0: Vector[Term] = Vector(A, B, a)
import TermData._

datT: monix.eval.Task[(TermState, Set[EquationNode])] = FlatMap(
  Async(<function2>, false, true, true),
  provingground.learning.TermData$$$Lambda$2565/339281181@523fc4f3
)

In [5]:
import monix.execution.Scheduler.Implicits.global
val td = datT.runSyncUnsafe()


Out[5]:
import monix.execution.Scheduler.Implicits.global

td: (TermState, Set[EquationNode]) = (
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×B) ↦ a,
          8.675006846432388E-4
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : B) ↦ @a,
          0.0010674443639559507
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : B×A) ↦ (```@a_1 , @a_2),
          3.7178600770424526E-4
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×A) ↦ (``@a_1 , @a_2),
          3.7178600770424526E-4
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ a,
          0.035508944319399785
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((`@a_1 , @a_2) : A×A) ↦ a,
          8.675006846432388E-4
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → A)) ↦ @a,
          5.872312326815773E-4
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → A)) ↦ @a,
          6.940005477145914E-4
        ),
        Weighted(
...

In [6]:
val (ns, eqs) = td


Out[6]:
ns: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×B) ↦ a,
        8.675006846432388E-4
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : B) ↦ @a,
        0.0010674443639559507
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : B×A) ↦ (```@a_1 , @a_2),
        3.7178600770424526E-4
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×A) ↦ (``@a_1 , @a_2),
        3.7178600770424526E-4
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ a,
        0.035508944319399785
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((`@a_1 , @a_2) : A×A) ↦ a,
        8.675006846432388E-4
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → A)) ↦ @a,
        5.872312326815773E-4
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → A)) ↦ @a,
        6.940005477145914E-4
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → B)) ↦ a,
...
eqs: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem((@a : B) ↦ @a, Terms),
              @a,
              Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
            ),
            a,
            Island(
              Typs,
              ConstRandVar(Typs),
              provingground.learning.ExpressionEval$$Lambda$2811/973096168@223eea22,
              Pi,
              EnterIsle
            )
          ),
          B,
          Island(
            Typs,
            ConstRandVar(Typs),
            provingground.learning.ExpressionEval$$Lambda$2811/973096168@1a048ff7,
            Pi,
            EnterIsle
          )
        ),
        A,
        Island(
          Typs,
          ConstRandVar(Typs),
          provingground.learning.ExpressionEval$$Lambda$2811/973096168@5c8d4da1,
          Pi,
          EnterIsle
        )
...

In [7]:
val atoms = (eqs.map(_.rhs).flatMap(Expression.varVals(_)) union eqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)


Out[7]:
atoms: Set[GeneratorVariables.Variable[Any]] = Set(
  InIsle(
    InIsle(
      InIsle(
        InIsle(
          Elem(B, Typs),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar((B → B)), Lambda, EnterIsle)
        ),
        a,
        Island(
          Typs,
          ConstRandVar(Typs),
          provingground.learning.ExpressionEval$$Lambda$2811/973096168@223eea22,
          Pi,
          EnterIsle
        )
      ),
      B,
      Island(
        Typs,
        ConstRandVar(Typs),
        provingground.learning.ExpressionEval$$Lambda$2811/973096168@1a048ff7,
        Pi,
        EnterIsle
      )
    ),
    A,
    Island(
      Terms,
      ConstRandVar(Terms),
      provingground.learning.ExpressionEval$$Lambda$2817/1951445643@4022bf60,
      Lambda,
      EnterIsle
    )
  ),
  InIsle(
    InIsle(
      InIsle(
...

In [8]:
import TermRandomVars._, GeneratorVariables._
val elemTerms = atoms.collect{case Elem(t: Term, Terms) => t}


Out[8]:
import TermRandomVars._, GeneratorVariables._

elemTerms: Set[Term] = Set(
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : B) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : B) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : B) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : A) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : B) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : B) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → A)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → A)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : B×A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((`@a_1 , @a_2) : A×A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×B) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((`@a_1 , @a_2) : B×B) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → A)) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → A)) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → B)) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → B)) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : B×A) ↦ (```@a_1 , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : B×B) ↦ (``@a_1 , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : A×B) ↦ (```@a_1 , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×A) ↦ (``@a_1 , @a_2)
)

In [9]:
elemTerms.exists(_.dependsOn(A))


Out[9]:
res8: Boolean = false

First check

None of the terms depends on the variables


In [10]:
atoms.size


Out[10]:
res9: Int = 4527

In [11]:
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))


Out[11]:
normEqs: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      InIsle(
        InIsle(
          InIsle(
            Elem(@a, Terms),
            @a,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7e094e58,
              AddVar(@a),
              Pi,
              EnterIsle
            )
          ),
          @b,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@170773c9,
            AddVar(𝒰 ),
            Lambda,
            EnterIsle
          )
        ),
        @a,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@5dbdcb12,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      )
    ),
    Product(
      Product(
...

In [12]:
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)


Out[12]:
normAtoms: Set[Variable[Any]] = Set(
  InIsle(
    InIsle(
      InIsle(
        InIsle(
          Elem((@b → @a), Typs),
          @b,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@6ede34ac,
            AddVar(@a),
            Sigma,
            EnterIsle
          )
        ),
        @a,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@4f610e6b,
          AddVar(@a),
          Lambda,
          EnterIsle
        )
      ),
      @b,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3079/68010752@439fdf6f,
        AddVar(𝒰 ),
        Lambda,
        EnterIsle
      )
    ),
    @a,
    Island(
      Typs,
      provingground.learning.TermRandomVars$$$Lambda$3079/68010752@6bb8503e,
      AddVar(𝒰 ),
...

In [13]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}


Out[13]:
normElemTerms: Set[Term] = Set(
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : B) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : B) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : B) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : B) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : A) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : B) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → A)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → A)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((`@a_1 , @a_2) : A×A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((`@a_1 , @a_2) : B×B) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : B×A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×B) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → A)) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → B)) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → B)) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → A)) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×A) ↦ (``@a_1 , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : B×A) ↦ (```@a_1 , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : A×B) ↦ (```@a_1 , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : B×B) ↦ (``@a_1 , @a_2)
)

In [14]:
elemTerms == normElemTerms


Out[14]:
res13: Boolean = true

Next conclusion

  • terms are generated correctly
  • however, this does not test deeper generation, for which we must generate with the equations.

In [15]:
val ts0 = TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))


Out[15]:
ts0: TermState = TermState(
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)

In [16]:
val ev = ExpressionEval.fromInitEqs(ts0, Equation.group(eqs), TermGenParams(), decayS = 0.75)


Out[16]:
ev: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@3a6afd74

In [17]:
val termsEv = ev.finalTerms


Out[17]:
termsEv: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : B×A) ↦ (```@a_1 , @a_2),
      0.023783361218616697
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×A) ↦ (``@a_1 , @a_2),
      0.023783346929568194
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : B×B) ↦ (``@a_1 , @a_2),
      0.023786541590912733
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : A×B) ↦ (```@a_1 , @a_2),
      0.023786520883480558
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → A)) ↦ @a,
      0.04758154345221369
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → A)) ↦ @a,
      0.04758142786902684
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → B)) ↦ @a,
      0.04759436016007325
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → B)) ↦ @a,
      0.04759419256878797
    ),
    Weighted(
...

In [18]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.75)


Out[18]:
evN: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@84900a0

In [19]:
val termsN = evN.finalTerms


Out[19]:
termsN: FiniteDistribution[Term] = FiniteDistribution(Vector())

In [20]:
evN.init


Out[20]:
res19: Map[Expression, Double] = Map(
  Coeff(
    BaseThenCondition(
      FiberProductMap(domOf, TermsWithTyp, Appln, TypFamilies, Terms),
      Typs,
      Restrict(TypOpt)
    )
  ) -> 0.1,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  Coeff(
    BaseThenCondition(
      FiberProductMap(typeOf(_), FuncsWithDomain, FlipAppn, Terms, Terms),
      AtCoord(FuncsWithDomain, A :: HNil),
      Restrict(FuncWithDom(A))
    )
  ) -> 0.1,
  IsleScale(a, Elem(a, AtCoord(TermsWithTyp, A :: HNil))) -> 0.7,
  IsleScale(@a, Elem(B, Typs)) -> 0.7,
  IsleScale(@a, Elem(B, Typs)) -> 0.7,
  IsleScale(@a, Elem(B, Typs)) -> 0.7,
  IsleScale(@a, Elem(B, Typs)) -> 0.7,
  IsleScale(@a, Elem(B, Typs)) -> 0.7,
  IsleScale(@a, Elem(B, Typs)) -> 0.7,
  InitialVal(Elem(Wrap(@a), Funcs)) -> 0.4285714285714286,
  InitialVal(Elem(Wrap(@a), Funcs)) -> 0.4285714285714286,
  IsleScale(@a, Elem(a, Terms)) -> 0.7,
  IsleScale(@a, Elem(a, Terms)) -> 0.7,
  IsleScale((@a_1 , @a_2), Elem((@a_1 , @a_2), Terms)) -> 0.7,
  Coeff(
    Island(
      AtCoord(FuncsWithDomain, (A → A) :: HNil),
      ConstRandVar(Terms),
      AddVar((A → A)),
      Lambda,
      EnterIsle
    )
  ) -> 0.1,
  Coeff(
    Island(
...

In [21]:
evN.maxRatio


Out[21]:
res20: Double = 1.01

In [22]:
evN.decay


Out[22]:
res21: Double = 0.75

In [23]:
evN.equations


Out[23]:
res22: Set[Equation] = Set(
  Equation(
    FinalVal(
      InIsle(
        InIsle(
          InIsle(
            Elem(@a, Terms),
            @a,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7e094e58,
              AddVar(@a),
              Pi,
              EnterIsle
            )
          ),
          @b,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@170773c9,
            AddVar(𝒰 ),
            Lambda,
            EnterIsle
          )
        ),
        @a,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@5dbdcb12,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      )
    ),
    Product(
      Product(
...

In [24]:
import ExpressionEval._


Out[24]:
import ExpressionEval._

defined function stableMap

In [25]:
val newMap = nextMap(evN.init, evN.equations, 0.5)


Out[25]:
newMap: Map[Expression, Double] = Map(
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem((@a_1 , @a_2), Terms),
            (@a_1 , @a_2),
            Island(
              Terms,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7c3d5089,
              AddVar(@b×@a),
              Lambda,
              EnterIsle
            )
          ),
          @a,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7726e262,
            AddVar(@a),
            Lambda,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@53e8f4a8,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
...

In [26]:
val ss : Stream[Map[Expression, Double]] = evN.init #:: ss.map(m =>  nextMap(m, evN.equations, 0.5))


Out[26]:
ss: Stream[Map[Expression, Double]] = [Map(Coeff(BaseThenCondition(FiberProductMap(domOf,TermsWithTyp,Appln,TypFamilies,Terms),Typs,Restrict(TypOpt))) -> 0.1, IsleScale(@a,@a ∈ Terms) -> 0.7, Coeff(BaseThenCondition(FiberProductMap(typeOf(_),FuncsWithDomain,FlipAppn,Terms,Terms),AtCoord(FuncsWithDomain,A :: HNil),Restrict(FuncWithDom(A)))) -> 0.1, IsleScale(a,a ∈ AtCoord(TermsWithTyp,A :: HNil)) -> 0.7, IsleScale(@a,B ∈ Typs) -> 0.7, IsleScale(@a,B ∈ Typs) -> 0.7, IsleScale(@a,B ∈ Typs) -> 0.7, IsleScale(@a,B ∈ Typs) -> 0.7, IsleScale(@a,B ∈ Typs) -> 0.7, IsleScale(@a,B ∈ Typs) -> 0.7, P₀(Wrap(@a) ∈ Funcs) -> 0.4285714285714286, P₀(Wrap(@a) ∈ Funcs) -> 0.4285714285714286, IsleScale(@a,a ∈ Terms) -> 0.7, IsleScale(@a,a ∈ Terms) -> 0.7, IsleScale(((@a_1) , (@a_2)),((@a_1) , (@a_2)) ∈ Terms) -> 0.7, Coeff(Island(AtCoord(FuncsWithDomain,(A) → (A) :: HNil),Terms,AddVar,Lambda,EnterIsle)) -> 0.1, Coeff(Island(AtCoord(FuncsWithDomain,(B) → (A) :: HNil),Terms,AddVar,Lambda,EnterIsle)) -> 0.1, Coeff(BaseThenCondition(ZipMapOpt(UnifApplnOpt,TypFamilies,Terms,Terms),TypFamilies,Restrict(TypFamilyOpt))) -> 0.1, IsleScale(((@a_1) , (@a_2)),B ∈ Typs) -> 0.7, Coeff(FlatMap(Typs,provingground.learning.TermGeneratorNodes$$Lambda$2472/1302149935@2f5e646f,Typs)) -> 0.1, P₀(Wrap(@a) ∈ Funcs) -> 0.4285714285714286, P₀(Wrap(@a) ∈ Funcs) -> 0.4285714285714286, IsleScale(A,A ∈ Typs) -> 0.7, Coeff(Island(AtCoord(TermsWithTyp,(B) → (A) :: HNil),AtCoord(TermsWithTyp,A :: HNil),AddVar,Lambda,EnterIsle)) -> 0.485, IsleScale(@a,B ∈ Typs) -> 0.7, Coeff(BaseThenCondition(FlatMap(Typs,LambdaIsle,Terms),Funcs,Restrict(FuncOpt))) -> 0.1, IsleScale(@a,a ∈ Terms) -> 0.7, Coeff(BaseThenCondition(ZipMapOpt(UnifApplnOpt,Funcs,Terms,Terms),AtCoord(TermsWithTyp,A :: HNil),Filter(WithTyp(typ)))) -> 0.1, IsleScale(a,Wrap(@a) ∈ Funcs) -> 0.7, IsleScale(a,Wrap(@a) ∈ Funcs) -> 0.7, Coeff(BaseThenCondition(FiberProductMap(typeOf(_),FuncsWithDomain,FlipAppn,Terms,Terms),AtCoord(TermsWithTyp,A :: HNil),Filter(WithTyp(typ)))) -> 0.1, IsleScale(@a,A ∈ Typs) -> 0.7, IsleScale(((@a_1) , (@a_2)),B ∈ Typs) -> 0.7, Coeff(Init(Typs)) -> 0.6, Coeff(BaseThenCondition(FiberProductMap(domOf,TermsWithTyp,Appln,TypFamilies,Terms),TypFamilies,Restrict(TypFamilyOpt))) -> 0.1, Coeff(Init(Funcs)) -> 0.55, IsleScale(@a,Wrap(@a) ∈ Funcs) -> 0.7, IsleScale(@a,Wrap(@a) ∈ Funcs) -> 0.7, Coeff(Map(Identity,Typs,TypsAndFamilies)) -> 0.5, IsleScale(@a,@a ∈ Terms) -> 0.7, IsleScale(@a,@a ∈ Terms) -> 0.7, Coeff(BaseThenCondition(FiberProductMap(typeOf(_),FuncsWithDomain,FlipAppn,Terms,Terms),TypFamilies,Restrict(TypFamilyOpt))) -> 0.1, Coeff(FiberProductMap(domOf,TermsWithTyp,Appln,Funcs,Terms)) -> 0.1, IsleScale(@a,A ∈ Typs) -> 0.7, IsleScale(@a,A ∈ Typs) -> 0.7, IsleScale(@a,A ∈ Typs) -> 0.7, IsleScale(@a,A ∈ Typs) -> 0.7, IsleScale(@a,A ∈ Typs) -> 0.7, IsleScale(@a,A ∈ Typs) -> 0.7, IsleScale(B,B ∈ Typs) -> 0.7, IsleScale(@a,@a ∈ Terms) -> 0.7, IsleScale(a,a ∈ Terms) -> 0.7, Coeff(Map(Identity,Typs,TargetTyps)) -> 0.30000000000000004, Coeff(BaseThenCondition(ZipFlatMap(TargetTyps,TermsWithTyp,Proj2,Terms),TypFamilies,Restrict(TypFamilyOpt))) -> 0.05, IsleScale(((@a_1) , (@a_...

In [27]:
val sizes = ss.map(_.keySet.size)


Out[27]:
sizes: Stream[Int] = [131 ...

In [28]:
sizes(2)


Out[28]:
res27: Int = 871

In [29]:
sizes.take(20).toVector


Out[29]:
res28: Vector[Int] = Vector(
  131,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871,
  871
)

In [30]:
val stable= ss.zip(ss.tail).map{case (m1, m2) => m1.keySet == m2.keySet}


Out[30]:
stable: Stream[Boolean] = [false ...

In [31]:
stable.take(20).toVector


Out[31]:
res30: Vector[Boolean] = Vector(
  false,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true,
  true
)

In [32]:
val ratios = ss.tail.zip(ss.tail.tail).map{case (m1, m2) => mapRatio(m1, m2)}


Out[32]:
ratios: Stream[Double] = [1.0 ...

In [33]:
ratios.take(20).toVector


Out[33]:
res32: Vector[Double] = Vector(
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0
)

Bug narrowed: we are getting NaN in mapRatios


In [34]:
val zeroes = ss.map(_.filter(_._2 == 0))


Out[34]:
zeroes: Stream[Map[Expression, Double]] = [Map() ...

In [35]:
zeroes.take(20).toVector


Out[35]:
res34: Vector[Map[Expression, Double]] = Vector(
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map(),
  Map()
)

In [36]:
val m1 = ss(1)
val m2 = ss(2)


Out[36]:
m1: Map[Expression, Double] = Map(
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem((@a_1 , @a_2), Terms),
            (@a_1 , @a_2),
            Island(
              Terms,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7c3d5089,
              AddVar(@b×@a),
              Lambda,
              EnterIsle
            )
          ),
          @a,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7726e262,
            AddVar(@a),
            Lambda,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@53e8f4a8,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
...
m2: Map[Expression, Double] = Map(
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem((@a_1 , @a_2), Terms),
            (@a_1 , @a_2),
            Island(
              Terms,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7c3d5089,
              AddVar(@b×@a),
              Lambda,
              EnterIsle
            )
          ),
          @a,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7726e262,
            AddVar(@a),
            Lambda,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@53e8f4a8,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
...

In [37]:
mapRatio(m1, m2)


Out[37]:
res36: Double = 1.0

In [38]:
val triple = m1.map{case (k, v) => (k, v, m2(k))}


Out[38]:
triple: collection.immutable.Iterable[(Expression, Double, Double)] = List(
  (
    InitialVal(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem((@a_1 , @a_2), Terms),
              (@a_1 , @a_2),
              Island(
                Terms,
                provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7c3d5089,
                AddVar(@b×@a),
                Lambda,
                EnterIsle
              )
            ),
            @a,
            Island(
              Terms,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7726e262,
              AddVar(@a),
              Lambda,
              EnterIsle
            )
          ),
          @b,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@53e8f4a8,
            AddVar(𝒰 ),
            Pi,
            EnterIsle
          )
        ),
        @a,
...

In [39]:
triple.filter(t => t._2 == 0 || t._3 == 0)


Out[39]:
res38: collection.immutable.Iterable[(Expression, Double, Double)] = List()

In [40]:
val rt = triple.map(t => (t._2/t._3, t._3/ t._2))


Out[40]:
rt: collection.immutable.Iterable[(Double, Double)] = List(
  (NaN, NaN),
  (1.0, 1.0),
  (1.0, 1.0),
  (NaN, NaN),
  (1.0, 1.0),
  (1.0, 1.0),
  (1.0, 1.0),
  (1.0, 1.0),
  (NaN, NaN),
  (1.0, 1.0),
  (1.0, 1.0),
  (1.0, 1.0),
  (1.0, 1.0),
  (1.0, 1.0),
  (NaN, NaN),
  (NaN, NaN),
  (1.0, 1.0),
  (NaN, NaN),
  (NaN, NaN),
  (1.0, 1.0),
  (1.0, 1.0),
  (1.0, 1.0),
  (NaN, NaN),
  (NaN, NaN),
  (1.0, 1.0),
  (1.0, 1.0),
  (NaN, NaN),
  (NaN, NaN),
  (1.0, 1.0),
  (1.0, 1.0),
  (1.0, 1.0),
  (NaN, NaN),
  (1.0, 1.0),
  (1.0, 1.0),
  (NaN, NaN),
  (1.0, 1.0),
  (1.0, 1.0),
  (1.0, 1.0),
...

In [41]:
triple.head._2
triple.head._3


Out[41]:
res40_0: Double = -0.7
res40_1: Double = NaN

In [42]:
triple.map(_._3)


Out[42]:
res41: collection.immutable.Iterable[Double] = List(
  NaN,
  1.0,
  1.0,
  NaN,
  1.0,
  1.0,
  1.0,
  1.0,
  NaN,
  1.0,
  1.0,
  1.0,
  1.0,
  1.0,
  NaN,
  NaN,
  1.0,
  NaN,
  NaN,
  1.0,
  0.1,
  1.0,
  NaN,
  NaN,
  1.0,
  1.0,
  NaN,
  NaN,
  1.0,
  1.0,
  1.0,
  NaN,
  1.0,
  0.7,
  NaN,
  1.0,
  1.0,
  1.0,
...

In [43]:
triple.filterNot(_._3 < 2)


Out[43]:
res42: collection.immutable.Iterable[(Expression, Double, Double)] = List(
  (
    InitialVal(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem((@a_1 , @a_2), Terms),
              (@a_1 , @a_2),
              Island(
                Terms,
                provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7c3d5089,
                AddVar(@b×@a),
                Lambda,
                EnterIsle
              )
            ),
            @a,
            Island(
              Terms,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7726e262,
              AddVar(@a),
              Lambda,
              EnterIsle
            )
          ),
          @b,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@53e8f4a8,
            AddVar(𝒰 ),
            Pi,
            EnterIsle
          )
        ),
        @a,
...

In [44]:
m1.values.toSet


Out[44]:
res43: Set[Double] = Set(
  0.485,
  0.16500000000000004,
  0.3,
  0.6,
  1.0,
  0.7,
  0.05,
  -0.7,
  0.1,
  0.5,
  0.55,
  0.4285714285714286,
  0.30000000000000004
)

In [45]:
m2.values.toSet


Out[45]:
res44: Set[Double] = Set(
  0.485,
  0.16500000000000004,
  0.6,
  0.29999999999999993,
  1.0,
  0.7,
  0.05,
  0.1,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
  NaN,
...

In [46]:
val steps  = normEqs.map(eq => recExp(m1, eq.rhs) -> eq)


Out[46]:
steps: Set[(Double, EquationNode)] = Set(
  (
    0.0,
    EquationNode(
      FinalVal(
        InIsle(
          InIsle(
            InIsle(
              Elem(@a, Typs),
              @a,
              Island(
                Terms,
                provingground.learning.TermRandomVars$$$Lambda$3079/68010752@41921e1d,
                AddVar(@a),
                Lambda,
                EnterIsle
              )
            ),
            @b,
            Island(
              Terms,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@75667428,
              AddVar(𝒰 ),
              Lambda,
              EnterIsle
            )
          ),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@4beb28bf,
            AddVar(𝒰 ),
            Pi,
            EnterIsle
          )
        )
...

In [47]:
steps.map(_._1)


Out[47]:
res46: Set[Double] = Set(0.0, 0.3, 1.0, -0.7)

In [48]:
val neg = steps.find(_._1 < 0)


Out[48]:
neg: Option[(Double, EquationNode)] = Some(
  (
    -0.7,
    EquationNode(
      InitialVal(
        InIsle(
          InIsle(
            InIsle(
              Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
              @a,
              Island(
                Typs,
                provingground.learning.TermRandomVars$$$Lambda$3079/68010752@408e8678,
                AddVar(@a),
                Pi,
                EnterIsle
              )
            ),
            @b,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@66c9287a,
              AddVar(𝒰 ),
              Pi,
              EnterIsle
            )
          ),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@d3fe061,
            AddVar(𝒰 ),
            Pi,
            EnterIsle
          )
        )
...

In [49]:
neg.get._2.rhs


Out[49]:
res48: Expression = Product(
  IsleScale(a, Elem(a, AtCoord(TermsWithTyp, A :: HNil))),
  Literal(-1.0)
)

In [51]:
val source = eqs.find(eq => TermData.isleNormalize(eq) == neg.get)


Out[51]:
source: Option[EquationNode] = None

In [52]:
val source = eqs.filter(eq => TermData.isleNormalize(eq).lhs == neg.get._2.lhs)


Out[52]:
source: Set[EquationNode] = Set()

In [53]:
normEqs.contains(neg.get._2)


Out[53]:
res52: Boolean = true

In [54]:
normEqs == eqs.map(eq => TermData.isleNormalize(eq))


Out[54]:
res53: Boolean = false

In [55]:
normEqs -- eqs.map(eq => TermData.isleNormalize(eq))


Out[55]:
res54: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      InIsle(
        InIsle(
          InIsle(
            Elem(@a, Terms),
            @a,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@7e094e58,
              AddVar(@a),
              Pi,
              EnterIsle
            )
          ),
          @b,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@170773c9,
            AddVar(𝒰 ),
            Lambda,
            EnterIsle
          )
        ),
        @a,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@5dbdcb12,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      )
    ),
    Product(
      Product(
...

In [57]:
val badEq = eqs.find(eq => TermData.isleNormalize(eq) != TermData.isleNormalize(eq)).get


Out[57]:
badEq: EquationNode = EquationNode(
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem((@a : B) ↦ @a, Terms),
            @a,
            Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
          ),
          a,
          Island(
            Typs,
            ConstRandVar(Typs),
            provingground.learning.ExpressionEval$$Lambda$2811/973096168@223eea22,
            Pi,
            EnterIsle
          )
        ),
        B,
        Island(
          Typs,
          ConstRandVar(Typs),
          provingground.learning.ExpressionEval$$Lambda$2811/973096168@1a048ff7,
          Pi,
          EnterIsle
        )
      ),
      A,
      Island(
        Typs,
        ConstRandVar(Typs),
        provingground.learning.ExpressionEval$$Lambda$2811/973096168@5c8d4da1,
        Pi,
        EnterIsle
      )
    )
  ),
...

In [58]:
val eq1 = TermData.isleNormalize(badEq)


Out[58]:
eq1: EquationNode = EquationNode(
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem((@a : @b) ↦ @a, Terms),
            @b,
            Island(
              Terms,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@26123324,
              AddVar(@a),
              Lambda,
              EnterIsle
            )
          ),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@653d968d,
            AddVar(@a),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@6f8d3f18,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
...

In [59]:
val eq2 = TermData.isleNormalize(badEq)


Out[59]:
eq2: EquationNode = EquationNode(
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem((@a : @b) ↦ @a, Terms),
            @b,
            Island(
              Terms,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@3666a4bd,
              AddVar(@a),
              Lambda,
              EnterIsle
            )
          ),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@5e754e5e,
            AddVar(@a),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@1f913741,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
...

In [60]:
eq1 == eq2


Out[60]:
res59: Boolean = false

In [61]:
eq1.rhs ==eq2.rhs


Out[61]:
res60: Boolean = false

In [62]:
eq1.rhs


Out[62]:
res61: Expression = Product(
  Coeff(FlatMap(Typs, LambdaIsle, Terms)),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem(@a, Terms),
              @a,
              Island(
                Terms,
                provingground.learning.TermRandomVars$$$Lambda$3079/68010752@27916bb7,
                AddVar(@b),
                Lambda,
                EnterIsle
              )
            ),
            @b,
            Island(
              Terms,
              provingground.learning.TermRandomVars$$$Lambda$3079/68010752@725de5a4,
              AddVar(@a),
              Lambda,
              EnterIsle
            )
          ),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@4205c6b,
            AddVar(@a),
            Pi,
            EnterIsle
          )
        ),
...

In [63]:
eq1.lhs == eq2.lhs


Out[63]:
res62: Boolean = false

In [64]:
eq1.lhs


Out[64]:
res63: Expression = FinalVal(
  InIsle(
    InIsle(
      InIsle(
        InIsle(
          Elem((@a : @b) ↦ @a, Terms),
          @b,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@26123324,
            AddVar(@a),
            Lambda,
            EnterIsle
          )
        ),
        @a,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@653d968d,
          AddVar(@a),
          Pi,
          EnterIsle
        )
      ),
      @b,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3079/68010752@6f8d3f18,
        AddVar(𝒰 ),
        Pi,
        EnterIsle
      )
    ),
    @a,
    Island(
      Typs,
      provingground.learning.TermRandomVars$$$Lambda$3079/68010752@5f19382c,
      AddVar(𝒰 ),
...

In [65]:
eq2.lhs


Out[65]:
res64: Expression = FinalVal(
  InIsle(
    InIsle(
      InIsle(
        InIsle(
          Elem((@a : @b) ↦ @a, Terms),
          @b,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3079/68010752@3666a4bd,
            AddVar(@a),
            Lambda,
            EnterIsle
          )
        ),
        @a,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@5e754e5e,
          AddVar(@a),
          Pi,
          EnterIsle
        )
      ),
      @b,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3079/68010752@1f913741,
        AddVar(𝒰 ),
        Pi,
        EnterIsle
      )
    ),
    @a,
    Island(
      Typs,
      provingground.learning.TermRandomVars$$$Lambda$3079/68010752@73b84868,
      AddVar(𝒰 ),
...

More narrowing: two applications of the isle normalization are taken as not equal.


In [67]:
import Expression._
val exp = badEq.lhs.asInstanceOf[FinalVal[Term]].variable


Out[67]:
import Expression._

exp: Variable[Term] = InIsle(
  InIsle(
    InIsle(
      InIsle(
        Elem((@a : B) ↦ @a, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
      ),
      a,
      Island(
        Typs,
        ConstRandVar(Typs),
        provingground.learning.ExpressionEval$$Lambda$2811/973096168@223eea22,
        Pi,
        EnterIsle
      )
    ),
    B,
    Island(
      Typs,
      ConstRandVar(Typs),
      provingground.learning.ExpressionEval$$Lambda$2811/973096168@1a048ff7,
      Pi,
      EnterIsle
    )
  ),
  A,
  Island(
    Typs,
    ConstRandVar(Typs),
    provingground.learning.ExpressionEval$$Lambda$2811/973096168@5c8d4da1,
    Pi,
    EnterIsle
  )
)

In [68]:
import TermRandomVars._
val n1 = isleNormalizeVars(exp, Vector())


Out[68]:
import TermRandomVars._

n1: Variable[Any] = InIsle(
  InIsle(
    InIsle(
      InIsle(
        Elem((@a : @b) ↦ @a, Terms),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@3be951c1,
          AddVar(@a),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3079/68010752@88f2631,
        AddVar(@a),
        Pi,
        EnterIsle
      )
    ),
    @b,
    Island(
      Typs,
      provingground.learning.TermRandomVars$$$Lambda$3079/68010752@56116fc1,
      AddVar(𝒰 ),
      Pi,
      EnterIsle
    )
  ),
  @a,
  Island(
    Typs,
    provingground.learning.TermRandomVars$$$Lambda$3079/68010752@4d1b67d3,
    AddVar(𝒰 ),
    Pi,
    EnterIsle
...

In [69]:
val n2 = isleNormalizeVars(exp, Vector())
n1 == n2


Out[69]:
n2: Variable[Any] = InIsle(
  InIsle(
    InIsle(
      InIsle(
        Elem((@a : @b) ↦ @a, Terms),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@77cb7,
          AddVar(@a),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3079/68010752@67bf7673,
        AddVar(@a),
        Pi,
        EnterIsle
      )
    ),
    @b,
    Island(
      Typs,
      provingground.learning.TermRandomVars$$$Lambda$3079/68010752@5c665cf7,
      AddVar(𝒰 ),
      Pi,
      EnterIsle
    )
  ),
  @a,
  Island(
    Typs,
    provingground.learning.TermRandomVars$$$Lambda$3079/68010752@5686714d,
    AddVar(𝒰 ),
    Pi,
    EnterIsle
...
res68_1: Boolean = false

In [70]:
val i1 = n1.asInstanceOf[InIsle[Term, TermState, Term, Term]]


Out[70]:
i1: InIsle[Term, TermState, Term, Term] = InIsle(
  InIsle(
    InIsle(
      InIsle(
        Elem((@a : @b) ↦ @a, Terms),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@3be951c1,
          AddVar(@a),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3079/68010752@88f2631,
        AddVar(@a),
        Pi,
        EnterIsle
      )
    ),
    @b,
    Island(
      Typs,
      provingground.learning.TermRandomVars$$$Lambda$3079/68010752@56116fc1,
      AddVar(𝒰 ),
      Pi,
      EnterIsle
    )
  ),
  @a,
  Island(
    Typs,
    provingground.learning.TermRandomVars$$$Lambda$3079/68010752@4d1b67d3,
    AddVar(𝒰 ),
    Pi,
    EnterIsle
...

In [71]:
val i2 = n2.asInstanceOf[InIsle[Term, TermState, Term, Term]]


Out[71]:
i2: InIsle[Term, TermState, Term, Term] = InIsle(
  InIsle(
    InIsle(
      InIsle(
        Elem((@a : @b) ↦ @a, Terms),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3079/68010752@77cb7,
          AddVar(@a),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3079/68010752@67bf7673,
        AddVar(@a),
        Pi,
        EnterIsle
      )
    ),
    @b,
    Island(
      Typs,
      provingground.learning.TermRandomVars$$$Lambda$3079/68010752@5c665cf7,
      AddVar(𝒰 ),
      Pi,
      EnterIsle
    )
  ),
  @a,
  Island(
    Typs,
    provingground.learning.TermRandomVars$$$Lambda$3079/68010752@5686714d,
    AddVar(𝒰 ),
    Pi,
    EnterIsle
...

In [72]:
i1.boat == i2.boat


Out[72]:
res71: Boolean = true

In [73]:
i1.isleVar == i2.isleVar


Out[73]:
res72: Boolean = false

In [74]:
i1.isle == i2.isle


Out[74]:
res73: Boolean = false

In [75]:
i1.isle


Out[75]:
res74: GeneratorNode.Island[Term, TermState, Term, Term] = Island(
  Typs,
  provingground.learning.TermRandomVars$$$Lambda$3079/68010752@4d1b67d3,
  AddVar(𝒰 ),
  Pi,
  EnterIsle
)

In [76]:
i2.isle


Out[76]:
res75: GeneratorNode.Island[Term, TermState, Term, Term] = Island(
  Typs,
  provingground.learning.TermRandomVars$$$Lambda$3079/68010752@5686714d,
  AddVar(𝒰 ),
  Pi,
  EnterIsle
)

In [77]:
i1.isle.initMap == i2.isle.initMap


Out[77]:
res76: Boolean = true

In [78]:
i1.isle.output == i2.isle.output


Out[78]:
res77: Boolean = true

In [79]:
i1.isle.islandOutput == i2.isle.islandOutput


Out[79]:
res78: Boolean = false

Bug localized

  • All the island outputs actually did not depend on boats, but were of the form ContantRandomVar(rv)
  • However in isleSub these were defined as lambdas.
  • should match here and correct.