Testing export and normalization of isles

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-8dd937ec3a.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$2576/557730498@68e8ba7d
)
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(
            Elem(B, Typs),
            a,
            Island(
              Typs,
              ConstRandVar(Typs),
              provingground.learning.ExpressionEval$$Lambda$2839/746465134@614ca8bb,
              Pi,
              EnterIsle
            )
          ),
          B,
          Island(
            Typs,
            ConstRandVar(Typs),
            provingground.learning.ExpressionEval$$Lambda$2839/746465134@7b57405b,
            Pi,
            EnterIsle
          )
        ),
        A,
        Island(
          Typs,
          ConstRandVar(Typs),
          provingground.learning.ExpressionEval$$Lambda$2839/746465134@55999e46,
          Pi,
          EnterIsle
        )
      )
    ),
    Product(
      Product(
...
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(
          InIsle(
            Elem(B, Typs),
            @a,
            Island(Typs, ConstRandVar(Typs), AddVar(A), Sigma, EnterIsle)
          ),
          @a,
          Island(Typs, ConstRandVar(Typs), AddVar(B), Sigma, EnterIsle)
        ),
        a,
        Island(
          Terms,
          ConstRandVar(Terms),
          provingground.learning.ExpressionEval$$Lambda$2845/686750468@24aba665,
          Lambda,
          EnterIsle
        )
      ),
      B,
      Island(
        Typs,
        ConstRandVar(Typs),
        provingground.learning.ExpressionEval$$Lambda$2839/746465134@7b57405b,
        Pi,
        EnterIsle
      )
    ),
    A,
    Island(
      Terms,
      ConstRandVar(Terms),
      provingground.learning.ExpressionEval$$Lambda$2845/686750468@535204e6,
      Lambda,
      EnterIsle
    )
...
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 : B) ā†¦ (@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) ā†¦ (@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 ā†’ B)) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (B ā†’ B)) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (B ā†’ A)) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ 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_1 , @a_2) : BƗA) ā†¦ 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 : (B ā†’ B)) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ B)) ā†¦ @a,
  (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),
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((``@a_1 , @a_2) : BƗB) ā†¦ (``@a_1 , @a_2),
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((```@a_1 , @a_2) : BƗ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 elemTyps = atoms.collect{case Elem(t: Typ[Term], Typs) => t}
Out[11]:
elemTyps: Set[Typ[Term]] = Set()
In [12]:
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))
Out[12]:
normEqs: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      InIsle(
        InIsle(
          Elem((@a ā†’ (@a ā†’ @bƗ@a)), Typs),
          @b,
          Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
        ),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(š’° ), Lambda, EnterIsle)
      )
    ),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2483/852504014@4c96c460,
          Typs
        )
      ),
      FinalVal(
        InIsle(
          InIsle(
            InIsle(
              Elem((@a ā†’ @bƗ@a), Typs),
              @a,
              Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
            ),
            @b,
            Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
          ),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(š’° ), Lambda, EnterIsle)
        )
      )
    )
  ),
...
In [13]:
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[13]:
normAtoms: Set[Variable[Any]] = Set(
  InIsle(
    InIsle(
      InIsle(
        Elem((@b ā†’ (@a ā†’ @a)), Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
      ),
      @b,
      Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
    ),
    @a,
    Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
  ),
  InIsle(
    InIsle(
      InIsle(
        Elem((@b ā†’ (@b ā†’ @a)), Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
      ),
      @b,
      Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
    ),
    @a,
    Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
  ),
  InIsle(
    InIsle(
      InIsle(
        Elem((@a ā†’ (@b ā†’ @a)), Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
      ),
      @b,
      Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
    ),
    @a,
    Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
...
In [14]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}
Out[14]:
normElemTerms: Set[Term] = Set(
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : B) ā†¦ (@a : B) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : B) ā†¦ (@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) ā†¦ (@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 : B) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ B)) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (B ā†’ B)) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (B ā†’ A)) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ A)) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((`@a_1 , @a_2) : AƗA) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((``@a_1 , @a_2) : BƗA) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((`@a_1 , @a_2) : BƗB) ā†¦ 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 ā†’ B)) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (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_1 , @a_2) : AƗB) ā†¦ (```@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ƗA) ā†¦ (``@a_1 , @a_2),
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((```@a_1 , @a_2) : BƗA) ā†¦ (```@a_1 , @a_2)
)
In [15]:
elemTerms == normElemTerms
Out[15]:
res14: Boolean = true

Next conclusion

  • terms are generated correctly
  • however, this does not test deeper generation, for which we must generate with the equations.
In [16]:
val ts0 = TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))
Out[16]:
ts0: TermState = TermState(
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(š’° , 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
In [17]:
val ev = ExpressionEval.fromInitEqs(ts0, Equation.group(eqs), TermGenParams(), decayS = 0.95)
Out[17]:
ev: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@772df45b
In [18]:
val termsT = ev.finalTerms
Out[18]:
termsT: 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 [19]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.95)
Out[19]:
evN: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@7329af08
In [20]:
val termsN = evN.finalTerms
Out[20]:
termsN: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((```@a_1 , @a_2) : BƗA) ā†¦ (```@a_1 , @a_2),
      0.021427818142670963
    ),
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((``@a_1 , @a_2) : BƗB) ā†¦ (``@a_1 , @a_2),
      0.021430696963074085
    ),
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((```@a_1 , @a_2) : AƗB) ā†¦ (```@a_1 , @a_2),
      0.021430678902601065
    ),
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((``@a_1 , @a_2) : AƗA) ā†¦ (``@a_1 , @a_2),
      0.02142780590265384
    ),
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ B)) ā†¦ @a,
      0.042880191056144476
    ),
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (B ā†’ A)) ā†¦ @a,
      0.042868736079918056
    ),
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ A)) ā†¦ @a,
      0.04286863716011596
    ),
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (B ā†’ B)) ā†¦ @a,
      0.04288033712339029
    ),
    Weighted(
...
In [21]:
termsT.support == termsN.support
Out[21]:
res20: Boolean = true
In [22]:
ExpressionEval.mapRatio(termsT.toMap, termsN.toMap)
Out[22]:
res21: Double = 4.6001650461794075
In [23]:
val bigT = termsT.support.maxBy(t => termsT(t) / termsN(t))
Out[23]:
bigT: Term = (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : B) ā†¦ a
In [24]:
termsT(bigT)
termsN(bigT)
Out[24]:
res23_0: Double = 0.03520116836582195
res23_1: Double = 0.031162283724873487
In [25]:
val bigN = termsT.support.maxBy(t => termsN(t) / termsT(t))
Out[25]:
bigN: Term = (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : A) ā†¦ (@a : A) ā†¦ a
In [26]:
termsT(bigN)
termsN(bigN)
Out[26]:
res25_0: Double = 0.002380181625229522
res25_1: Double = 0.01094922831593934

Partial bug fix

  • the crash has stopped
  • however, it is clear that variable names are being reused incorrectly.
  • this bug remains even after correction to nextName
In [27]:
val ns = lp.nextState.runSyncUnsafe()
Out[27]:
ns: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(((@a_1 , @a_2) : AƗB) ā†¦ a, 8.675006846432388E-4),
      Weighted((@a : B) ā†¦ (@a : B) ā†¦ @a, 0.0010674443639559507),
      Weighted(((`@a_1 , @a_2) : BƗA) ā†¦ (`@a_1 , @a_2), 3.7178600770424526E-4),
      Weighted(((`@a_1 , @a_2) : AƗA) ā†¦ (`@a_1 , @a_2), 3.7178600770424526E-4),
      Weighted((@a : B) ā†¦ a, 0.035508944319399785),
      Weighted(((@a_1 , @a_2) : AƗA) ā†¦ a, 8.675006846432388E-4),
      Weighted((@a : (A ā†’ A)) ā†¦ @a, 5.872312326815773E-4),
      Weighted((@a : (B ā†’ A)) ā†¦ @a, 6.940005477145914E-4),
      Weighted((@a : (A ā†’ B)) ā†¦ a, 0.001370206209590347),
      Weighted((@a : (B ā†’ B)) ā†¦ a, 0.0016193346113340464),
      Weighted((@a : A) ā†¦ @a, 0.02245098635849324),
      Weighted((@a : A) ā†¦ (@a : A) ā†¦ @a, 0.0011041153249291451),
      Weighted(((`@a_1 , @a_2) : BƗB) ā†¦ (`@a_1 , @a_2), 3.7178600770424526E-4),
      Weighted((@a : A) ā†¦ (@a : A) ā†¦ a, 0.0010608166847358453),
      Weighted((@a : (A ā†’ A)) ā†¦ @a(a), 3.558977167767136E-4),
      Weighted((@a : A) ā†¦ (@a : B) ā†¦ @a, 6.494796028994972E-4),
      Weighted((@a : B) ā†¦ (@a : A) ā†¦ @a, 4.3953591457009735E-4),
      Weighted(a, 0.8658912103781063),
      Weighted((@a : B) ā†¦ (@a : B) ā†¦ a, 0.0010255838006635605),
      Weighted((@a : (A ā†’ A)) ā†¦ a, 0.001370206209590347),
      Weighted((@a : (B ā†’ A)) ā†¦ a, 0.0016193346113340464),
      Weighted((@a : (B ā†’ B)) ā†¦ @a, 6.940005477145914E-4),
      Weighted((@a : (A ā†’ B)) ā†¦ @a, 5.872312326815773E-4),
      Weighted((@a : A) ā†¦ (@a : B) ā†¦ a, 0.0010608166847358453),
      Weighted((@a : B) ā†¦ (@a : A) ā†¦ a, 0.0010255838006635605),
      Weighted(((`@a_1 , @a_2) : AƗB) ā†¦ (`@a_1 , @a_2), 3.7178600770424526E-4),
      Weighted((@a : A) ā†¦ a, 0.03721737508977956),
      Weighted((@a : B) ā†¦ @a, 0.016205076100067474),
      Weighted((@a : A) ā†¦ (@a : B) ā†¦ @a, 4.546357220296481E-4),
      Weighted((@a : B) ā†¦ (@a : A) ā†¦ @a, 6.279084493858533E-4),
      Weighted(((@a_1 , @a_2) : BƗA) ā†¦ a, 8.675006846432388E-4),
      Weighted(((@a_1 , @a_2) : BƗB) ā†¦ a, 8.675006846432388E-4),
      Weighted((@a : (A ā†’ B)) ā†¦ @a(a), 3.558977167767136E-4)
    )
  ),
  FiniteDistribution(
...

The error is clearly present here too. The next check is where we change the context.

In [28]:
val ts1 = ts.copy(context = Context.Empty)
Out[28]:
ts1: 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()),
  Empty
)
In [29]:
val lp1 = lp.copy(initState = ts1)
Out[29]:
lp1: 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()),
    Empty
  ),
  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 [30]:
val ns1 = lp1.nextState.runSyncUnsafe()
Out[30]:
ns1: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(((@a_1 , @a_2) : AƗB) ā†¦ a, 8.671859432529369E-4),
      Weighted((@a : B) ā†¦ (@b : B) ā†¦ @b, 6.25946582994212E-4),
      Weighted((@a : B) ā†¦ (@b : B) ā†¦ @a, 4.3816260809594835E-4),
      Weighted(((`@a_1 , @a_2) : BƗA) ā†¦ (`@a_1 , @a_2), 3.71651118536973E-4),
      Weighted(((`@a_1 , @a_2) : AƗA) ā†¦ (`@a_1 , @a_2), 3.71651118536973E-4),
      Weighted((@a : B) ā†¦ a, 0.0384282501336959),
      Weighted(((@a_1 , @a_2) : AƗA) ā†¦ a, 8.671859432529369E-4),
      Weighted((@a : (A ā†’ A)) ā†¦ @a, 5.870181769712191E-4),
      Weighted((@a : (B ā†’ A)) ā†¦ @a, 6.937487546023499E-4),
      Weighted((@a : (B ā†’ B)) ā†¦ a, 0.0016187470940721494),
      Weighted((@a : (A ā†’ B)) ā†¦ a, 0.0013697090795995112),
      Weighted((@b : A) ā†¦ @b, 0.012675323748495152),
      Weighted((@a : A) ā†¦ (@b : A) ā†¦ @b, 6.588580589777157E-4),
      Weighted((@a : A) ā†¦ (@b : A) ā†¦ @a, 4.612006412844011E-4),
      Weighted(((`@a_1 , @a_2) : BƗB) ā†¦ (`@a_1 , @a_2), 3.71651118536973E-4),
      Weighted((@a : A) ā†¦ (@b : A) ā†¦ a, 0.0010761348296636024),
      Weighted((@a : (A ā†’ A)) ā†¦ @a(a), 3.557685921037692E-4),
      Weighted((@a : A) ā†¦ (@a : B) ā†¦ @a, 6.588580589777157E-4),
      Weighted((@a : B) ā†¦ (@a : A) ā†¦ @a, 4.3816260809594835E-4),
      Weighted(a, 0.8741931716134901),
      Weighted((@a : B) ā†¦ (@b : B) ā†¦ a, 0.001022379418890546),
      Weighted((@a : (A ā†’ A)) ā†¦ a, 0.0013697090795995112),
      Weighted((@a : (B ā†’ A)) ā†¦ a, 0.0016187470940721494),
      Weighted((@a : (B ā†’ B)) ā†¦ @a, 6.937487546023499E-4),
      Weighted((@a : (A ā†’ B)) ā†¦ @a, 5.870181769712191E-4),
      Weighted((@a : A) ā†¦ (@a : B) ā†¦ a, 0.0010761348296636024),
      Weighted((@a : B) ā†¦ (@a : A) ā†¦ a, 0.001022379418890546),
      Weighted(((`@a_1 , @a_2) : AƗB) ā†¦ (`@a_1 , @a_2), 3.71651118536973E-4),
      Weighted((@b : A) ā†¦ a, 0.03855347011506094),
      Weighted((@a : B) ā†¦ @a, 0.013379088467587383),
      Weighted((@a : A) ā†¦ (@a : B) ā†¦ @a, 4.612006412844011E-4),
      Weighted((@a : B) ā†¦ (@a : A) ā†¦ @a, 6.25946582994212E-4),
      Weighted(((@a_1 , @a_2) : BƗA) ā†¦ a, 8.671859432529369E-4),
      Weighted(((@a_1 , @a_2) : BƗB) ā†¦ a, 8.671859432529369E-4),
      Weighted((@a : (A ā†’ B)) ā†¦ @a(a), 3.557685921037692E-4)
    )
...
In [31]:
ns1.terms.support -- ns.terms.support
Out[31]:
res30: Set[Term] = Set((@a : B) ā†¦ (@b : B) ā†¦ @a, (@a : A) ā†¦ (@b : A) ā†¦ @a)
In [32]:
ns.terms.support -- ns1.terms.support
Out[32]:
res31: Set[Term] = Set()
In [33]:
val t = ns.terms.pmf(13).elem
Out[33]:
t: Term = (@a : A) ā†¦ (@a : A) ā†¦ a
In [35]:
val tOpt = ns1.terms.support.find(x => x == t)
Out[35]:
tOpt: Option[Term] = Some((@a : A) ā†¦ (@b : A) ā†¦ a)
In [36]:
tOpt.get == t
Out[36]:
res35: Boolean = true
In [37]:
t == tOpt.get
Out[37]:
res36: Boolean = true
In [38]:
val x = nextVar(A, Vector(A, B, a))
Out[38]:
x: Term = @a
In [39]:
val ctx = ts.context.addVariable(x)
val y = nextVar(A, ctx.variables)
Out[39]:
ctx: Context.AppendVariable[Term] = AppendVariable(
  AppendVariable(AppendVariable(AppendVariable(Empty, A), B), a),
  @a
)
y: Term = @a
In [40]:
ts.context
Out[40]:
res39: Context = AppendVariable(AppendVariable(AppendVariable(Empty, A), B), a)
In [41]:
ts.context.variables
Out[41]:
res40: Vector[Term] = Vector(A, B, (A : š’° ) ā†¦ a)
In [42]:
ctx.variables
Out[42]:
res41: Vector[Term] = Vector(A, B, (A : š’° ) ā†¦ a, (A : š’° ) ā†¦ @a)

It is evident what caused the error - the variable in a context changed its type. The code has been corrected to no longer use contexts, and the stuff should be run without contexts.