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-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).sharpen(10)
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-5,
  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$2561/530697066@56ff73d9
)
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,
          5.425255561327946E-4
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A β†’ AΓ—A)) ↦ @a,
          2.3669326838587427E-5
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B β†’ AΓ—A)) ↦ @a,
          2.3669326838587427E-5
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : B) ↦ (@a : A) ↦ @a,
          3.2378133230521586E-5
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : A) ↦ (@a : B) ↦ @a,
          4.625447604360225E-5
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : B) ↦ (@a : B) ↦ @a,
          2.2664693261365112E-5
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ (@a : B) ↦ @a,
          3.0017119505275946E-5
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : B) ↦ (@a : A) ↦ @a,
          4.2881599293251334E-5
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ (@a : A) ↦ @a,
          2.1011983653693162E-5
...
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,
        5.425255561327946E-4
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A β†’ AΓ—A)) ↦ @a,
        2.3669326838587427E-5
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B β†’ AΓ—A)) ↦ @a,
        2.3669326838587427E-5
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : B) ↦ (@a : A) ↦ @a,
        3.2378133230521586E-5
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : A) ↦ (@a : B) ↦ @a,
        4.625447604360225E-5
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@a : B) ↦ (@a : B) ↦ @a,
        2.2664693261365112E-5
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ (@a : B) ↦ @a,
        3.0017119505275946E-5
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : B) ↦ (@a : A) ↦ @a,
        4.2881599293251334E-5
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ (@a : A) ↦ @a,
        2.1011983653693162E-5
      ),
...
eqs: Set[EquationNode] = Set(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem(B, Typs),
              @a,
              Island(
                Terms,
                ConstRandVar(Terms),
                AddVar((B β†’ A)),
                Lambda,
                EnterIsle
              )
            ),
            a,
            Island(
              Typs,
              ConstRandVar(Typs),
              provingground.learning.ExpressionEval$$Lambda$2810/440174345@22a1b85c,
              Pi,
              EnterIsle
            )
          ),
          B,
          Island(
            Terms,
            ConstRandVar(Terms),
            provingground.learning.ExpressionEval$$Lambda$2816/1279821339@290d6093,
            Lambda,
            EnterIsle
          )
        ),
        A,
        Island(
...
In [7]:
eqs.map(_.lhs)
Out[7]:
res6: Set[Expression] = Set(
  FinalVal(
    InIsle(
      InIsle(
        Elem((a : A) ↦ ((@a_1 , (@a_2_1 , @a_2_2)) : BΓ—AΓ—B) ↦ a, Terms),
        B,
        Island(
          Terms,
          ConstRandVar(Terms),
          provingground.learning.ExpressionEval$$Lambda$2816/1279821339@290d6093,
          Lambda,
          EnterIsle
        )
      ),
      A,
      Island(
        Typs,
        ConstRandVar(Typs),
        provingground.learning.ExpressionEval$$Lambda$2810/440174345@5d8c4ef0,
        Pi,
        EnterIsle
      )
    )
  ),
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem((@a_1 , (@a_2_1 , @a_2_2)), Terms),
            (@a_1 , (@a_2_1 , @a_2_2)),
            Island(Terms, ConstRandVar(Terms), AddVar(AΓ—BΓ—B), Lambda, EnterIsle)
          ),
          a,
          Island(
            Terms,
            ConstRandVar(Terms),
            provingground.learning.ExpressionEval$$Lambda$2816/1279821339@67dc8f...
In [8]:
eqs.map(_.rhs)
Out[8]:
res7: Set[Expression] = Set(
  Product(
    IsleScale(a, Elem(Wrap(@a), Funcs)),
    InitialVal(
      InIsle(
        InIsle(
          Elem(Wrap(@a), Funcs),
          B,
          Island(
            Terms,
            ConstRandVar(Terms),
            provingground.learning.ExpressionEval$$Lambda$2816/1279821339@290d6093,
            Lambda,
            EnterIsle
          )
        ),
        A,
        Island(
          Terms,
          ConstRandVar(Terms),
          provingground.learning.ExpressionEval$$Lambda$2816/1279821339@fda9dce,
          Lambda,
          EnterIsle
        )
      )
    )
  ),
  Product(
    IsleScale(a, Elem(Wrap(@a), Funcs)),
    InitialVal(
      InIsle(
        InIsle(
          Elem(Wrap(@a), Funcs),
          B,
          Island(
            Terms,
            ConstRandVar(Terms),
            provingground.learning.ExpressionEval$$Lambda$2816/1279821339@290d60...
In [9]:
val atoms = (eqs.map(_.rhs).flatMap(Expression.varVals(_)) union eqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[9]:
atoms: Set[GeneratorVariables.Variable[Any]] = Set(
  InIsle(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem(B, Typs),
              @a,
              Island(Typs, ConstRandVar(Typs), AddVar(B), Sigma, EnterIsle)
            ),
            @a,
            Island(Typs, ConstRandVar(Typs), AddVar(B), Pi, EnterIsle)
          ),
          @a,
          Island(Typs, ConstRandVar(Typs), AddVar(A), Sigma, EnterIsle)
        ),
        a,
        Island(
          Typs,
          ConstRandVar(Typs),
          provingground.learning.ExpressionEval$$Lambda$2810/440174345@22a1b85c,
          Pi,
          EnterIsle
        )
      ),
      B,
      Island(
        Terms,
        ConstRandVar(Terms),
        provingground.learning.ExpressionEval$$Lambda$2816/1279821339@290d6093,
        Lambda,
        EnterIsle
      )
    ),
    A,
    Island(
      Typs,
      ConstRandVar(Typs),
...
In [10]:
import TermRandomVars._, GeneratorVariables._
val elemTerms = atoms.collect{case Elem(t: Term, Terms) => t}
Out[10]:
import TermRandomVars._, GeneratorVariables._

elemTerms: Set[Term] = Set(
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : BΓ—AΓ—A) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : AΓ—BΓ—B) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : AΓ—AΓ—B) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((``@a_1_1 , @a_1_2) , @a_2) : AΓ—AΓ—A) ↦ ((``@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((``@a_1_1 , @a_1_2) , @a_2) : BΓ—BΓ—B) ↦ ((``@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : BΓ—BΓ—A) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : AΓ—BΓ—A) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : BΓ—AΓ—B) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (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 : A) ↦ (@a : A) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@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 : 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 : ((A β†’ A) β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : ((A β†’ B) β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : ((B β†’ A) β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : ((B β†’ B) β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (AΓ—A β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (AΓ—B β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (BΓ—B β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (BΓ—A β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : ((A β†’ B) β†’ A)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : ((A β†’ A) β†’ A)) ↦ a,
...
In [11]:
elemTerms.exists(_.dependsOn(A))
Out[11]:
res10: Boolean = false

First checkΒΆ

None of the terms depends on the variables

In [12]:
atoms.size
Out[12]:
res11: Int = 31252
In [13]:
val elemTyps = atoms.collect{case Elem(t: Typ[Term], Typs) => t}
Out[13]:
elemTyps: Set[Typ[Term]] = Set()
In [14]:
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))
Out[14]:
normEqs: Set[EquationNode] = Set(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              InIsle(
                Elem(@a, Terms),
                @a,
                Island(
                  Terms,
                  provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@714e5352,
                  AddVar(@b),
                  Lambda,
                  EnterIsle
                )
              ),
              @b,
              Island(
                AtCoord(FuncsWithDomain, @a :: HNil),
                provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@419a2b43,
                AddVar(@a),
                Lambda,
                EnterIsle
              )
            ),
            @a,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@888b3f3,
              AddVar(@a),
              Pi,
              EnterIsle
            )
          ),
...
In [17]:
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[17]:
normAtoms: Set[Variable[Any]] = Set(
  InIsle(
    InIsle(
      InIsle(
        InIsle(
          Elem(@b, Typs),
          (@a_1 , @a_2),
          Island(
            TypFamilies,
            provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@62a7fbf6,
            AddVar(@bΓ—@b),
            Lambda,
            EnterIsle
          )
        ),
        @a,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@1aa1e3c8,
          AddVar(@a),
          Lambda,
          EnterIsle
        )
      ),
      @b,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@451eab90,
        AddVar(𝒰 ),
        Lambda,
        EnterIsle
      )
    ),
    @a,
    Island(
      Terms,
      provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@668d73c6,
...
In [18]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}
Out[18]:
normElemTerms: Set[Term] = Set(
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : AΓ—AΓ—B) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((``@a_1_1 , @a_1_2) , @a_2) : AΓ—AΓ—A) ↦ ((``@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : BΓ—AΓ—A) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((``@a_1_1 , @a_1_2) , @a_2) : BΓ—BΓ—B) ↦ ((``@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : AΓ—BΓ—A) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : AΓ—BΓ—B) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : BΓ—BΓ—A) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (((```@a_1_1 , @a_1_2) , @a_2) : BΓ—AΓ—B) ↦ ((```@a_1_1 , @a_1_2) , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@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 : A) ↦ 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 : 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 β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : ((A β†’ A) β†’ A)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (AΓ—B β†’ A)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (AΓ—A β†’ A)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : ((A β†’ B) β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (BΓ—B β†’ A)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : ((A β†’ A) β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : ((A β†’ B) β†’ A)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (BΓ—B β†’ B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (BΓ—A β†’ A)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (AΓ—A β†’ B)) ↦ a,
...
In [19]:
show(normEqs.take(10).map(_.lhs))

Set(
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@a, Typs),
            @b,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@685aabf4,
              AddVar(@a),
              Sigma,
              EnterIsle
            )
          ),
          @a,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@41b62c6,
            AddVar(@a),
            Lambda,
            EnterIsle
          )
        ),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@75a178fe,
          AddVar(𝒰 ),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@7bb9b5b0,
        AddVar(𝒰 ),
        Pi,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          Elem((@bΓ—@a β†’ @aΓ—@b), Typs),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@66ee709,
            AddVar(@a),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@2831bf05,
          AddVar(𝒰 ),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@67ea8897,
        AddVar(𝒰 ),
        Lambda,
        EnterIsle
      )
    )
  ),
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem(@a, Terms),
              @a,
              Island(
                Terms,
                provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@714e5352,
                AddVar(@b),
                Lambda,
                EnterIsle
              )
            ),
            @b,
            Island(
              AtCoord(FuncsWithDomain, @a :: HNil),
              provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@419a2b43,
              AddVar(@a),
              Lambda,
              EnterIsle
            )
          ),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@888b3f3,
            AddVar(@a),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@678f250f,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@64d83e6f,
        AddVar(𝒰 ),
        Pi,
        EnterIsle
      )
    )
  ),
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              InIsle(
                Elem(@a, Typs),
                @b,
                Island(
                  Typs,
                  provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@296f1e9f,
                  AddVar(@b),
                  Pi,
                  EnterIsle
                )
              ),
              @b,
              Island(
                Typs,
                provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@fb94f3,
                AddVar(@a),
                Pi,
                EnterIsle
              )
            ),
            @a,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@69a3c9ea,
              AddVar(@b),
              Sigma,
              EnterIsle
            )
          ),
          @a,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@3f62238e,
            AddVar(@a),
            Lambda,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@6e28491b,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@32a81421,
        AddVar(𝒰 ),
        Pi,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          Elem(Wrap((@a : (@b β†’ @b)) ↦ @b), TypFamilies),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@4cb07ad,
            AddVar(@a),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@541c4fca,
          AddVar(𝒰 ),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@72978067,
        AddVar(𝒰 ),
        Lambda,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          Elem(Wrap((@a : @a) ↦ @b), TypFamilies),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@56173bbd,
            AddVar(@a),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@2702ae3d,
          AddVar(𝒰 ),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@382206bd,
        AddVar(𝒰 ),
        Lambda,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              InIsle(
                Elem(@b, Typs),
                @a,
                Island(
                  Typs,
                  provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@7a90a5b6,
                  AddVar(@b),
                  Pi,
                  EnterIsle
                )
              ),
              @c,
              Island(
                Typs,
                provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@3b6bc172,
                AddVar(@a),
                Sigma,
                EnterIsle
              )
            ),
            @b,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@799727e7,
              AddVar(@a),
              Pi,
              EnterIsle
            )
          ),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@7136f5ab,
            AddVar(@a),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@e74432e,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@6b7173c3,
        AddVar(𝒰 ),
        Pi,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem(@b, Typs),
              @a,
              Island(
                Typs,
                provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@7d068fd2,
                AddVar(@b),
                Sigma,
                EnterIsle
              )
            ),
            @a,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@45f6e04f,
              AddVar((@b β†’ @b)),
              Sigma,
              EnterIsle
            )
          ),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@4c86be98,
            AddVar(@a),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@57cf6750,
          AddVar(𝒰 ),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@1efe1a64,
        AddVar(𝒰 ),
        Lambda,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          Elem((@b β†’ @a)Γ—@bΓ—@a, Typs),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@37dfa841,
            AddVar(@a),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@4cfa9f5a,
          AddVar(𝒰 ),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@1c2e13cc,
        AddVar(𝒰 ),
        Pi,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(((@a β†’ @b) β†’ @a), Typs),
            @a,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@4fea7803,
              AddVar(@b),
              Pi,
              EnterIsle
            )
          ),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@6534b94b,
            AddVar(@a),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@17ec87af,
          AddVar(𝒰 ),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3125/2103660574@6af628b2,
        AddVar(𝒰 ),
        Lambda,
        EnterIsle
      )
    )
  )
)
In [20]:
elemTerms == normElemTerms
Out[20]:
res19: Boolean = true

Next conclusionΒΆ

  • terms are generated correctly
  • however, this does not test deeper generation, for which we must generate with the equations.
In [21]:
val ts0 = TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))
Out[21]:
ts0: TermState = TermState(
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
In [22]:
val ev = ExpressionEval.fromInitEqs(ts0, Equation.group(eqs), TermGenParams(), decayS = 0.95)
Out[22]:
ev: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@1f8cff5e
In [23]:
val termsT = ev.finalTerms
Out[23]:
termsT: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , (@a_2_1 , @a_2_2)) : AΓ—AΓ—B) ↦ a,
      0.00407379896217516
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((`@a_1 , (@a_2_1 , @a_2_2)) : BΓ—BΓ—B) ↦ a,
      0.004073799161465585
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((`@a_1 , (@a_2_1 , @a_2_2)) : AΓ—AΓ—A) ↦ a,
      0.004073779791043477
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , (@a_2_1 , @a_2_2)) : AΓ—BΓ—A) ↦ a,
      0.00407377984164196
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , (@a_2_1 , @a_2_2)) : BΓ—AΓ—B) ↦ a,
      0.004073799085112612
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , (@a_2_1 , @a_2_2)) : BΓ—BΓ—A) ↦ a,
      0.004073779925013815
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , (@a_2_1 , @a_2_2)) : AΓ—BΓ—B) ↦ a,
      0.004073799038380095
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , (@a_2_1 , @a_2_2)) : BΓ—AΓ—A) ↦...
In [28]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.5)
Out[28]:
evN: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@167cf5f
In [29]:
val termsN = evN.finalTerms

Interrupted!
  scala.runtime.Statics.anyHash(Statics.java:122)
  scala.util.hashing.MurmurHash3.productHash(MurmurHash3.scala:68)
  scala.util.hashing.MurmurHash3$.productHash(MurmurHash3.scala:215)
  scala.runtime.ScalaRunTime$._hashCode(ScalaRunTime.scala:149)
  provingground.learning.TermGeneratorNodes$AddVar.hashCode(TermGeneratorNodes.scala:83)
  scala.runtime.Statics.anyHash(Statics.java:122)
  scala.util.hashing.MurmurHash3.productHash(MurmurHash3.scala:68)
  scala.util.hashing.MurmurHash3$.productHash(MurmurHash3.scala:215)
  scala.runtime.ScalaRunTime$._hashCode(ScalaRunTime.scala:149)
  provingground.learning.GeneratorNode$Island.hashCode(GeneratorNode.scala:470)
  scala.runtime.Statics.anyHash(Statics.java:122)
  scala.util.hashing.MurmurHash3.productHash(MurmurHash3.scala:68)
  scala.util.hashing.MurmurHash3$.productHash(MurmurHash3.scala:215)
  scala.runtime.ScalaRunTime$._hashCode(ScalaRunTime.scala:149)
  provingground.learning.GeneratorVariables$InIsle.hashCode(GeneratorVariables.scala:175)
  scala.runtime.Statics.anyHash(Statics.java:122)
  scala.util.hashing.MurmurHash3.productHash(MurmurHash3.scala:68)
  scala.util.hashing.MurmurHash3$.productHash(MurmurHash3.scala:215)
  scala.runtime.ScalaRunTime$._hashCode(ScalaRunTime.scala:149)
  provingground.learning.GeneratorVariables$InIsle.hashCode(GeneratorVariables.scala:175)
  scala.runtime.Statics.anyHash(Statics.java:122)
  scala.util.hashing.MurmurHash3.productHash(MurmurHash3.scala:68)
  scala.util.hashing.MurmurHash3$.productHash(MurmurHash3.scala:215)
  scala.runtime.ScalaRunTime$._hashCode(ScalaRunTime.scala:149)
  provingground.learning.Expression$FinalVal.hashCode(GeneratorVariables.scala:310)
  scala.runtime.Statics.anyHash(Statics.java:122)
  scala.util.hashing.MurmurHash3.productHash(MurmurHash3.scala:68)
  scala.util.hashing.MurmurHash3$.productHash(MurmurHash3.scala:215)
  scala.runtime.ScalaRunTime$._hashCode(ScalaRunTime.scala:149)
  provingground.learning.Expression$Product.hashCode(GeneratorVariables.scala:347)
  scala.runtime.Statics.anyHash(Statics.java:122)
  scala.collection.immutable.HashMap.elemHashCode(HashMap.scala:87)
  scala.collection.immutable.HashMap.computeHash(HashMap.scala:96)
  scala.collection.immutable.HashMap.get(HashMap.scala:56)
  scala.collection.MapLike.getOrElse(MapLike.scala:129)
  scala.collection.MapLike.getOrElse$(MapLike.scala:129)
  scala.collection.AbstractMap.getOrElse(Map.scala:63)
  provingground.learning.ExpressionEval$.recExp(ExpressionEval.scala:103)
  provingground.learning.ExpressionEval$.stabRecExp(ExpressionEval.scala:126)
  provingground.learning.ExpressionEval$.$anonfun$nextMap$1(ExpressionEval.scala:141)
  provingground.learning.ExpressionEval$$$Lambda$2819/1865196807.apply(Unknown Source)
  scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:237)
  scala.collection.TraversableLike$$Lambda$125/973576304.apply(Unknown Source)
  scala.collection.immutable.HashSet$HashSet1.foreach(HashSet.scala:321)
  scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:977)
  scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:977)
  scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:977)
  scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:977)
  scala.collection.TraversableLike.map(TraversableLike.scala:237)
  scala.collection.TraversableLike.map$(TraversableLike.scala:230)
  scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:51)
  scala.collection.SetLike.map(SetLike.scala:104)
  scala.collection.SetLike.map$(SetLike.scala:104)
  scala.collection.AbstractSet.map(Set.scala:51)
  provingground.learning.ExpressionEval$.nextMap(ExpressionEval.scala:141)
  provingground.learning.ExpressionEval$.stableMap(ExpressionEval.scala:186)
  provingground.learning.ExpressionEval.finalDist(ExpressionEval.scala:424)
  provingground.learning.ExpressionEval.finalDist$(ExpressionEval.scala:423)
  provingground.learning.ExpressionEval$$anon$2.finalDist$lzycompute(ExpressionEval.scala:231)
  provingground.learning.ExpressionEval$$anon$2.finalDist(ExpressionEval.scala:231)
  provingground.learning.ExpressionEval.finalTerms(ExpressionEval.scala:448)
  provingground.learning.ExpressionEval.finalTerms$(ExpressionEval.scala:446)
  provingground.learning.ExpressionEval$$anon$2.finalTerms$lzycompute(ExpressionEval.scala:231)
  provingground.learning.ExpressionEval$$anon$2.finalTerms(ExpressionEval.scala:231)
  ammonite.$sess.cmd28$Helper.<init>(cmd28.sc:1)
  ammonite.$sess.cmd28$.<init>(cmd28.sc:7)
  ammonite.$sess.cmd28$.<clinit>(cmd28.sc:-1)
In [26]:
normEqs.size
Out[26]:
res25: Int = 61844
In [27]:
eqs.size
Out[27]:
res26: Int = 61844

Preliminary conclusionΒΆ

  • The computation of the evolved state with equations hung, even with a large decay.
  • This may be because of a bug.
  • Most of the time was spent with equality, but may be because of looping.
  • We will run again a simpler version and try to further diagnose.