Testing export and normalization of isles

This is after correcting the issue with context variables. There are still a couple of things to test and correct.

  • No final types in equations
  • Check if difference in weights after normalizing is due to an error.

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-294d1cadfc.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))
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()),
  Empty
)
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()),
    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 [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$2552/15947442@7b258736
)
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.671859432529369E-4
        ),
        Weighted((B : 𝒰 ) ↦ (@a : B) ↦ (@b : B) ↦ @b, 6.25946582994212E-4),
        Weighted((B : 𝒰 ) ↦ (@a : B) ↦ (@b : B) ↦ @a, 4.3816260809594835E-4),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ ((```@a_1 , @a_2) : B×A) ↦ (```@a_1 , @a_2),
          3.71651118536973E-4
        ),
        Weighted(
          (A : 𝒰 ) ↦ ((``@a_1 , @a_2) : A×A) ↦ (``@a_1 , @a_2),
          3.71651118536973E-4
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ a,
          0.0384282501336959
        ),
        Weighted(
          (A : 𝒰 ) ↦ (a : A) ↦ ((`@a_1 , @a_2) : A×A) ↦ a,
          8.671859432529369E-4
        ),
        Weighted((A : 𝒰 ) ↦ (@a : (A → A)) ↦ @a, 5.870181769712191E-4),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (@a : (B → A)) ↦ @a,
          6.937487546023499E-4
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → B)) ↦ a,
          0.0016187470940721494
        ),
        Weighted(
          (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → B)) ↦ a,
          0.0013697090795995112
        ),
...
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.671859432529369E-4
      ),
      Weighted((B : 𝒰 ) ↦ (@a : B) ↦ (@b : B) ↦ @b, 6.25946582994212E-4),
      Weighted((B : 𝒰 ) ↦ (@a : B) ↦ (@b : B) ↦ @a, 4.3816260809594835E-4),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ ((```@a_1 , @a_2) : B×A) ↦ (```@a_1 , @a_2),
        3.71651118536973E-4
      ),
      Weighted(
        (A : 𝒰 ) ↦ ((``@a_1 , @a_2) : A×A) ↦ (``@a_1 , @a_2),
        3.71651118536973E-4
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ a,
        0.0384282501336959
      ),
      Weighted(
        (A : 𝒰 ) ↦ (a : A) ↦ ((`@a_1 , @a_2) : A×A) ↦ a,
        8.671859432529369E-4
      ),
      Weighted((A : 𝒰 ) ↦ (@a : (A → A)) ↦ @a, 5.870181769712191E-4),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (@a : (B → A)) ↦ @a,
        6.937487546023499E-4
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → B)) ↦ a,
        0.0016187470940721494
      ),
      Weighted(
        (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → B)) ↦ a,
        0.0013697090795995112
      ),
      Weighted((A : 𝒰 ) ↦ (@b : A) ↦ @b, 0.012675323748495152),
...
eqs: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      InIsle(
        InIsle(
          InIsle(
            Elem(((B → B) → B), Typs),
            a,
            Island(
              Typs,
              ConstRandVar(Typs),
              provingground.learning.ExpressionEval$$Lambda$2810/475781992@5e143423,
              Pi,
              EnterIsle
            )
          ),
          B,
          Island(
            Typs,
            ConstRandVar(Typs),
            provingground.learning.ExpressionEval$$Lambda$2810/475781992@3a467786,
            Pi,
            EnterIsle
          )
        ),
        A,
        Island(
          Typs,
          ConstRandVar(Typs),
          provingground.learning.ExpressionEval$$Lambda$2810/475781992@431b2d9b,
          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(
      Elem((a : A) ↦ A, Terms),
      B,
      Island(
        Typs,
        ConstRandVar(Typs),
        provingground.learning.ExpressionEval$$Lambda$2810/475781992@3a467786,
        Pi,
        EnterIsle
      )
    ),
    A,
    Island(
      Terms,
      ConstRandVar(Terms),
      provingground.learning.ExpressionEval$$Lambda$2816/103690594@3df53352,
      Lambda,
      EnterIsle
    )
  ),
  InIsle(
    InIsle(
      Elem((A → B×B×B), Typs),
      B,
      Island(
        Terms,
        ConstRandVar(Terms),
        provingground.learning.ExpressionEval$$Lambda$2816/103690594@775bfcc7,
        Lambda,
        EnterIsle
      )
    ),
    A,
    Island(
      Typs,
      ConstRandVar(Typs),
      provingground.learning.ExpressionEval$$Lambda$2810/475781992@431b2d9b,
...
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) ↦ (@b : A) ↦ @b,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@b : A) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@b : A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@b : B) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@b : B) ↦ @b,
  (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 : 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 : B) ↦ (@b : B) ↦ 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×A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×B) ↦ 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 : 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 : (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×B) ↦ (``@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×A) ↦ (``@a_1 , @a_2),
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : A×B) ↦ (```@a_1 , @a_2)
)
In [9]:
elemTerms.exists(_.dependsOn(A))
Out[9]:
res8: Boolean = false

First checks

  • None of the terms depends on the variables
  • The duplication in generated variables has stopped.
In [10]:
atoms.size
Out[10]:
res9: Int = 4637
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(
    InitialVal(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem(@a, Typs),
              @a,
              Island(
                Typs,
                ConstRandVar(Typs),
                AddVar((@b → @a)),
                Sigma,
                EnterIsle
              )
            ),
            @a,
            Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
          ),
          @b,
          Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
        ),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(𝒰 ), Pi, EnterIsle)
      )
    ),
    Product(
      IsleScale(@a, Elem(A, Typs)),
      InitialVal(
        InIsle(
          InIsle(
            InIsle(
              Elem(@a, Typs),
              @a,
              Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
            ),
            @b,
            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((@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)
  ),
  InIsle(
    InIsle(
      InIsle(
        Elem((@a → (@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)
...
In [14]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}
Out[14]:
normElemTerms: Set[Term] = Set(
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@b : B) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@b : B) ↦ @b,
  (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 : B) ↦ (@a : A) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@b : A) ↦ @b,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@b : A) ↦ @a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@b : 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) ↦ (@b : B) ↦ 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×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]:
show(normEqs.take(10).map(_.lhs))
Set(
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem(@a, Typs),
              @b,
              Island(Typs, ConstRandVar(Typs), AddVar(@b), Sigma, EnterIsle)
            ),
            @a,
            Island(Typs, ConstRandVar(Typs), AddVar(@b), Pi, EnterIsle)
          ),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Typs),
            @a,
            Island(
              TypFamilies,
              ConstRandVar(TypsAndFamilies),
              AddVar((@b → @b)),
              Lambda,
              EnterIsle
            )
          ),
          @a,
          Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
        ),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Typs),
            @a,
            Island(
              TypFamilies,
              ConstRandVar(TypsAndFamilies),
              AddVar((@a → @b)),
              Lambda,
              EnterIsle
            )
          ),
          @a,
          Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
        ),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
    )
  ),
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@a, Typs),
            @a,
            Island(
              Typs,
              ConstRandVar(Typs),
              AddVar((@b → @a)),
              Sigma,
              EnterIsle
            )
          ),
          @a,
          Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
        ),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      ),
      @a,
      Island(Typs, ConstRandVar(Typs), AddVar(𝒰 ), Pi, EnterIsle)
    )
  ),
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@a, Typs),
            @a,
            Island(
              Typs,
              ConstRandVar(Typs),
              AddVar((@a → @a)),
              Sigma,
              EnterIsle
            )
          ),
          @a,
          Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
        ),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      ),
      @a,
      Island(Typs, ConstRandVar(Typs), AddVar(𝒰 ), Pi, EnterIsle)
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          Elem((@a : @a) ↦ (@b : @a) ↦ @a, Terms),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      ),
      @a,
      Island(Typs, ConstRandVar(Typs), AddVar(𝒰 ), Pi, EnterIsle)
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          Elem((@a : @a) ↦ (@b : @a) ↦ @b, Terms),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      ),
      @a,
      Island(Typs, ConstRandVar(Typs), AddVar(𝒰 ), Pi, EnterIsle)
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          Elem((@a : (@b → @b)) ↦ @a, Terms),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      ),
      @a,
      Island(Typs, ConstRandVar(Typs), AddVar(𝒰 ), Pi, EnterIsle)
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          Elem((@a : (@a → @b)) ↦ @a, Terms),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      ),
      @a,
      Island(Typs, ConstRandVar(Typs), AddVar(𝒰 ), Pi, EnterIsle)
    )
  ),
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem(@b, Typs),
              @b,
              Island(Typs, ConstRandVar(Typs), AddVar(@a), Sigma, EnterIsle)
            ),
            @a,
            Island(Typs, ConstRandVar(Typs), AddVar(@b), Sigma, EnterIsle)
          ),
          @a,
          Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
        ),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
    )
  )
)
In [16]:
elemTerms == normElemTerms
Out[16]:
res15: Boolean = true

Next conclusion

  • terms are generated correctly
  • however, this does not test deeper generation, for which we must generate with the equations.
In [17]:
val ts0 = TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))
Out[17]:
ts0: TermState = TermState(
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
In [18]:
val ev = ExpressionEval.fromInitEqs(ts0, Equation.group(eqs), TermGenParams(), decayS = 0.95)
Out[18]:
ev: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@2941afd9
In [19]:
val termsT = ev.finalTerms
Out[19]:
termsT: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : A×B) ↦ (```@a_1 , @a_2),
      0.023962625587406663
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : B×B) ↦ (``@a_1 , @a_2),
      0.023962646594319292
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : B×A) ↦ (```@a_1 , @a_2),
      0.023959446907723708
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×A) ↦ (``@a_1 , @a_2),
      0.023959432340384276
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → A)) ↦ @a,
      0.04793389196886914
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → B)) ↦ @a,
      0.04794678649334244
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → B)) ↦ @a,
      0.04794661644290413
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → A)) ↦ @a,
      0.04793377410149417
    ),
    Weighted(
...
In [20]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.95)
Out[20]:
evN: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@53d5e88c
In [21]:
val termsN = evN.finalTerms
Out[21]:
termsN: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : B×A) ↦ (```@a_1 , @a_2),
      0.021400851824832142
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : B×B) ↦ (``@a_1 , @a_2),
      0.02140371915246402
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×A) ↦ (``@a_1 , @a_2),
      0.021400839225495592
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : A×B) ↦ (```@a_1 , @a_2),
      0.021403700759429465
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → A)) ↦ @a,
      0.042814840303911104
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → B)) ↦ @a,
      0.04282634834944096
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → B)) ↦ @a,
      0.04282649716482151
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (B → A)) ↦ @a,
      0.04281494217902027
    ),
    Weighted(
...
In [22]:
termsT.support == termsN.support
Out[22]:
res21: Boolean = true
In [23]:
ExpressionEval.mapRatio(termsT.toMap, termsN.toMap)
Out[23]:
res22: Double = 3.931792873252659
In [24]:
val bigT = termsT.support.maxBy(t => termsT(t) / termsN(t))
Out[24]:
bigT: Term = (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ a
In [25]:
termsT(bigT)
termsN(bigT)
Out[25]:
res24_0: Double = 0.03557308639905361
res24_1: Double = 0.031137651884931093
In [26]:
val bigN = termsT.support.maxBy(t => termsN(t) / termsT(t))
Out[26]:
bigN: Term = (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@b : A) ↦ a
In [27]:
termsT(bigN)
termsN(bigN)
Out[27]:
res26_0: Double = 0.002398174997951145
res26_1: Double = 0.009429127365757023

Bug fixes

  • the crash has stopped
  • names are now used correctly.
In [28]:
val ns = lp.nextState.runSyncUnsafe()
Out[28]:
ns: 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 [29]:
val x = nextVar(A, Vector())
Out[29]:
x: Term = @a
In [30]:
val ctx = Context.Empty.addVariable(x)
val y = nextVar(A, ctx.variables)
Out[30]:
ctx: Context.AppendVariable[Term] = AppendVariable(Empty, @a)
y: Term = @b

Even with contexts, variable names are correct. We now investigate type generation.

In [31]:
ns.typs
Out[31]:
res30: FiniteDistribution[Typ[Term]] = FiniteDistribution(
  Vector(
    Weighted(A, 0.4236958282176533),
    Weighted(B×A, 0.008376687159819445),
    Weighted(A×A, 0.008376687159819445),
    Weighted(B×B×B, 4.3628578957392953E-4),
    Weighted(B×(B → A), 6.980572633182873E-4),
    Weighted(B×(A → A), 6.980572633182873E-4),
    Weighted((B → A)×B, 7.479184964124504E-4),
    Weighted((A → A)×B, 7.479184964124504E-4),
    Weighted(B×A×B, 3.4902863165914364E-4),
    Weighted((B → B×A), 7.456359374203474E-4),
    Weighted((A → B×A), 7.456359374203474E-4),
    Weighted(A×A×A, 3.4902863165914364E-4),
    Weighted(B×(B → B), 6.980572633182873E-4),
    Weighted(B×(A → B), 6.980572633182873E-4),
    Weighted((B → B)×A, 7.479184964124504E-4),
    Weighted((A → B)×A, 7.479184964124504E-4),
    Weighted(B×A×B, 4.3628578957392953E-4),
    Weighted((B → B)×B, 7.479184964124504E-4),
    Weighted((A → B)×B, 7.479184964124504E-4),
    Weighted(A×B, 0.008376687159819445),
    Weighted(B×B×A, 3.4902863165914364E-4),
    Weighted(A×A×A, 4.3628578957392953E-4),
    Weighted((B → B×B), 7.456359374203474E-4),
    Weighted((A → B×B), 7.456359374203474E-4),
    Weighted(B, 0.4236958282176533),
    Weighted((B → A×B), 7.456359374203474E-4),
    Weighted((A → A×B), 7.456359374203474E-4),
    Weighted(A×B×B, 4.3628578957392953E-4),
    Weighted((B → (B → A)), 0.001278233035577738),
    Weighted((B → (A → A)), 0.001278233035577738),
    Weighted((A → (A → A)), 0.001278233035577738),
    Weighted((A → (B → A)), 0.001278233035577738),
    Weighted((B → B), 0.017895262498088333),
    Weighted((A×B → B), 5.877589404665492E-4),
    Weighted((A×A → B), 5.877589404665492E-4),
    Weighted((A → B), 0.017895262498088333),
    Weighted((B×A → B), 5.877589404665492E-4),
...
In [32]:
val eq0 = lp.equations.runSyncUnsafe()
Out[32]:
eq0: Set[Equation] = Set(
  Equation(
    InitialVal(
      InIsle(
        Elem(A, Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar((B → A)), Sigma, EnterIsle)
      )
    ),
    Product(IsleScale(@a, Elem(A, Typs)), InitialVal(Elem(A, Typs)))
  ),
  Equation(
    InitialVal(
      InIsle(
        Elem(A, Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar((A → A)), Sigma, EnterIsle)
      )
    ),
    Product(IsleScale(@a, Elem(A, Typs)), InitialVal(Elem(A, Typs)))
  ),
  Equation(
    FinalVal(
      InIsle(
        Elem((@a : B) ↦ a, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
      )
    ),
    Sum(
      Sum(
        Sum(
          Product(
            Product(
              Coeff(
                BaseThenCondition(
                  FlatMap(Typs, LambdaIsle, Terms),
                  Funcs,
                  Restrict(FuncOpt)
...
In [33]:
import Expression._
val varsEq0 = eq0.map(_.lhs).flatMap(varVals).map(_.variable)
Out[33]:
import Expression._

varsEq0: Set[Variable[Any]] = Set(
  InIsle(
    Elem((@b : B) ↦ @a, Terms),
    @a,
    Island(Terms, ConstRandVar(Terms), AddVar(B), Lambda, EnterIsle)
  ),
  InIsle(
    Elem((B → B), Typs),
    @a,
    Island(Typs, ConstRandVar(Typs), AddVar(A), Pi, EnterIsle)
  ),
  InIsle(
    Elem((A → B), Typs),
    @a,
    Island(Typs, ConstRandVar(Typs), AddVar(A), Pi, EnterIsle)
  ),
  InIsle(
    InIsle(
      Elem(@a, Terms),
      @a,
      Island(
        AtCoord(FuncsWithDomain, A :: HNil),
        ConstRandVar(Terms),
        AddVar(A),
        Lambda,
        EnterIsle
      )
    ),
    @a,
    Island(Terms, ConstRandVar(Terms), AddVar(B), Lambda, EnterIsle)
  ),
  Elem(B×A, TargetTyps),
  InIsle(
    Elem(B, Typs),
    @a,
    Island(Typs, ConstRandVar(Typs), AddVar((A → A)), Sigma, EnterIsle)
  ),
  InIsle(
    Elem(B, Typs),
...
In [34]:
val elemsEq0 = varsEq0.collect{case el  @ Elem(_, _) => el}
Out[34]:
elemsEq0: Set[Elem[Any]] = Set(
  Elem(B×A, TargetTyps),
  Elem((A → B×B), Typs),
  Elem((B → B×B), Typs),
  Elem(B×A×A, Typs),
  Elem(A×A, Typs),
  Elem((A → B×A), Typs),
  Elem((B → B×A), Typs),
  Elem((@a : B) ↦ @a, Terms),
  Elem((B → B)×B, Typs),
  Elem((A → B)×B, Typs),
  Elem((@a : B) ↦ @a, AtCoord(TermsWithTyp, (B → B) :: HNil)),
  Elem(((`@a_1 , @a_2) : A×A) ↦ (`@a_1 , @a_2), Terms),
  Elem(A×B×A, Typs),
  Elem(A×A×B, Typs),
  Elem(B, Terms),
  Elem(Wrap((@a : B) ↦ B), TypFamilies),
  Elem(Wrap((@a : (B → A)) ↦ a), AtCoord(FuncsWithDomain, (B → A) :: HNil)),
  Elem(Wrap((@a : (A → A)) ↦ a), AtCoord(FuncsWithDomain, (A → A) :: HNil)),
  Elem(B×A×B, Typs),
  Elem((@a : (B → A)) ↦ a, Terms),
  Elem((@a : (A → A)) ↦ a, Terms),
  Elem(((`@a_1 , @a_2) : B×A) ↦ (`@a_1 , @a_2), Terms),
  Elem(((@a_1 , @a_2) : B×A) ↦ a, Terms),
  Elem((@a : A) ↦ (@b : A) ↦ a, Terms),
  Elem(((@a_1 , @a_2) : B×B) ↦ a, Terms),
  Elem(Wrap((@a : A) ↦ (@b : A) ↦ @b), AtCoord(FuncsWithDomain, A :: HNil)),
  Elem(A×(B → A), Typs),
  Elem(A×(A → A), Typs),
  Elem(B×A, Typs),
  Elem((@a : A) ↦ a, Terms),
  Elem(Wrap((@a : A) ↦ B), TypFamilies),
  Elem((@a : (A → B)) ↦ @a, Terms),
  Elem((@a : (B → B)) ↦ @a, Terms),
  Elem(B×B, TargetTyps),
  Elem(A×(A → B), Typs),
  Elem(A×(B → B), Typs),
  Elem(Wrap((@a : A) ↦ a), Funcs),
  Elem(a, Terms),
...

clearly there are types here.

In [35]:
ev.finalTyps
Out[35]:
res34: FiniteDistribution[Typ[Term]] = FiniteDistribution(Vector())
In [36]:
val typEqs0 = eq0.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[36]:
typEqs0: Set[Equation] = Set(
  Equation(
    FinalVal(Elem(A×B×A, Typs)),
    Sum(
      Product(
        Product(
          Coeff(
            FlatMap(
              Typs,
              provingground.learning.TermGeneratorNodes$$Lambda$2460/1589832331@3ae6bebb,
              Typs
            )
          ),
          FinalVal(Elem(A, Typs))
        ),
        FinalVal(Elem(A×B×A, Typs))
      ),
      Product(
        Coeff(
          FlatMap(
            Typs,
            provingground.learning.TermGeneratorNodes$$Lambda$2460/1589832331@3ae6bebb,
            Typs
          )
        ),
        FinalVal(
          InIsle(
            Elem(B×A, Typs),
            @a,
            Island(Typs, ConstRandVar(Typs), AddVar(A), Sigma, EnterIsle)
          )
        )
      )
    )
  ),
  Equation(
    FinalVal(Elem((B → B), Typs)),
...
In [37]:
val ev0 = lp.expressionEval.runSyncUnsafe()
Out[37]:
ev0: ExpressionEval = provingground.learning.ExpressionEval$$anon$1@2769e4d7
In [38]:
ev0.equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[38]:
res37: Set[Equation] = Set(
  Equation(
    FinalVal(Elem(A×B×A, Typs)),
    Sum(
      Product(
        Product(
          Coeff(
            FlatMap(
              Typs,
              provingground.learning.TermGeneratorNodes$$Lambda$2460/1589832331@3ae6bebb,
              Typs
            )
          ),
          FinalVal(Elem(A, Typs))
        ),
        FinalVal(Elem(A×B×A, Typs))
      ),
      Product(
        Coeff(
          FlatMap(
            Typs,
            provingground.learning.TermGeneratorNodes$$Lambda$2460/1589832331@3ae6bebb,
            Typs
          )
        ),
        FinalVal(
          InIsle(
            Elem(B×A, Typs),
            @a,
            Island(Typs, ConstRandVar(Typs), AddVar(A), Sigma, EnterIsle)
          )
        )
      )
    )
  ),
  Equation(
    FinalVal(Elem((B → B), Typs)),
...
In [39]:
ev0.piExportEquations(a).collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[39]:
res38: Set[Equation] = Set(
  Equation(
    FinalVal(Elem((A → B×B×B), Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2459/1429135242@449263fc,
          Typs
        )
      ),
      FinalVal(
        InIsle(
          Elem(B×B×B, Typs),
          a,
          Island(
            Typs,
            ConstRandVar(Typs),
            provingground.learning.ExpressionEval$$Lambda$2810/475781992@4557fa2f,
            Pi,
            EnterIsle
          )
        )
      )
    )
  ),
  Equation(
    FinalVal(Elem((A → B×A×B), Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2459/1429135242@449263fc,
          Typs
        )
      ),
...
In [40]:
ev0.relVariable(a).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[40]:
res39: Set[Equation] = Set(
  Equation(
    FinalVal(Elem((A → B×A), Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2459/1429135242@449263fc,
          Typs
        )
      ),
      FinalVal(
        InIsle(
          Elem(B×A, Typs),
          a,
          Island(
            Typs,
            ConstRandVar(Typs),
            provingground.learning.ExpressionEval$$Lambda$2810/475781992@31b80c0b,
            Pi,
            EnterIsle
          )
        )
      )
    )
  ),
  Equation(
    FinalVal(Elem((A → A×B×A), Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2459/1429135242@449263fc,
          Typs
        )
      ),
...
In [41]:
ExpressionEval.export(ev0, Vector(A, B, a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[41]:
res40: Set[Equation] = Set()
In [42]:
ExpressionEval.export(ev0, Vector(B, a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[42]:
res41: Set[Equation] = Set()
In [43]:
ExpressionEval.export(ev0, Vector(B)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[43]:
res42: Set[Equation] = Set(
  Equation(
    FinalVal(Elem(∏(B : 𝒰 ){ B×A×A }, Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2459/1429135242@449263fc,
          Typs
        )
      ),
      FinalVal(
        InIsle(
          Elem(B×A×A, Typs),
          B,
          Island(
            Typs,
            ConstRandVar(Typs),
            provingground.learning.ExpressionEval$$Lambda$2810/475781992@7e202b84,
            Pi,
            EnterIsle
          )
        )
      )
    )
  ),
  Equation(
    FinalVal(Elem(∏(B : 𝒰 ){ B×B×A }, Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2459/1429135242@449263fc,
          Typs
        )
      ),
...
In [44]:
ExpressionEval.export(ev0, Vector(A, B)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[44]:
res43: Set[Equation] = Set(
  Equation(
    FinalVal(Elem(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ A×B } }, Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2459/1429135242@449263fc,
          Typs
        )
      ),
      FinalVal(
        InIsle(
          Elem(∏(B : 𝒰 ){ A×B }, Typs),
          A,
          Island(
            Typs,
            ConstRandVar(Typs),
            provingground.learning.ExpressionEval$$Lambda$2810/475781992@4c4231a8,
            Pi,
            EnterIsle
          )
        )
      )
    )
  ),
  Equation(
    FinalVal(Elem(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ A×B×B } }, Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2459/1429135242@449263fc,
          Typs
        )
      ),
...
In [45]:
ExpressionEval.export(ev0, Vector(A, a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[45]:
res44: Set[Equation] = Set()
In [46]:
ExpressionEval.export(ev0, Vector(a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[46]:
res45: Set[Equation] = Set(
  Equation(
    FinalVal(Elem((A → A×(B → A)), Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2459/1429135242@449263fc,
          Typs
        )
      ),
      FinalVal(
        InIsle(
          Elem(A×(B → A), Typs),
          a,
          Island(
            Typs,
            ConstRandVar(Typs),
            provingground.learning.ExpressionEval$$Lambda$2810/475781992@33b73c04,
            Pi,
            EnterIsle
          )
        )
      )
    )
  ),
  Equation(
    FinalVal(Elem((A → A×(A → A)), Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2459/1429135242@449263fc,
          Typs
        )
      ),
...
In [47]:
val ev1 = ExpressionEval.export(ev0, Vector(a))
Out[47]:
ev1: ExpressionEval = provingground.learning.ExpressionEval$$anon$9@7d5cce46
In [48]:
ExpressionEval.export(ev1, Vector(B)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[48]:
res47: Set[Equation] = Set()
In [49]:
ev1.piExportEquations(B).collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[49]:
res48: Set[Equation] = Set()
In [50]:
ev1.finalTyps
Out[50]:
res49: FiniteDistribution[Typ[Term]] = FiniteDistribution(Vector())
In [51]:
ev0.init
Out[51]:
res50: 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(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(A, Typs)) -> 0.5,
  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,
  InitialVal(Elem(B, Typs)) -> 0.5,
  IsleScale(@b, Elem(@a, Terms)) -> 0.7,
  Coeff(
    Island(
      AtCoord(FuncsWithDomain, (B → A) :: HNil),
      ConstRandVar(Terms),
      AddVar((B → A)),
      Lambda,
      EnterIsle
    )
  ) -> 0.1,
...
In [52]:
ev1.init
Out[52]:
res51: 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(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(A, Typs)) -> 0.5,
  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,
  InitialVal(Elem(B, Typs)) -> 0.5,
  IsleScale(@b, Elem(@a, Terms)) -> 0.7,
  Coeff(
    Island(
      AtCoord(FuncsWithDomain, (B → A) :: HNil),
      ConstRandVar(Terms),
      AddVar((B → A)),
      Lambda,
      EnterIsle
    )
  ) -> 0.1,
...
In [53]:
ev1.equations.collect{case eq @ Equation(FinalVal(Elem(A, Typs)), _) => eq}
Out[53]:
res52: Set[Equation] = Set()
In [54]:
ev0.equations.collect{case eq @ Equation(FinalVal(Elem(A, Typs)), _) => eq}
Out[54]:
res53: Set[Equation] = Set(
  Equation(
    FinalVal(Elem(A, Typs)),
    Sum(
      Sum(
        Sum(
          Quotient(
            FinalVal(Elem(A, Terms)),
            FinalVal(Event(Terms, Restrict(TypOpt)))
          ),
          Product(
            Product(
              Coeff(
                FlatMap(
                  TypFamilies,
                  provingground.learning.TermGeneratorNodes$$Lambda$2461/1728401242@5e1fa44c,
                  Typs
                )
              ),
              FinalVal(Elem(a, AtCoord(TermsWithTyp, A :: HNil)))
            ),
            FinalVal(Elem(A, Typs))
          )
        ),
        Product(Coeff(Init(Typs)), InitialVal(Elem(A, Typs)))
      ),
      Product(
        Product(
          Coeff(
            FlatMap(
              TypFamilies,
              provingground.learning.TermGeneratorNodes$$Lambda$2461/1728401242@5e1fa44c,
              Typs
            )
          ),
          FinalVal(Elem(Wrap((@a : A) ↦ A), TypFamilies))
        ),
...
In [55]:
A.dependsOn(a)
Out[55]:
res54: Boolean = false

Bug diagnosed

  • There is no equation for FinalVal(Elem(A, Typs)) once we export by a, as all equations are assumed to be in island.
  • Correction: If an equation is independent of the variable, it is exported as it is.
  • However: We should not take too long to check independence. We test this.
In [56]:
def varDepends(t: Term)(v: Variable[_]) : Boolean = 
    v match {
      case Elem(element: Term, randomVar) => element.dependsOn(t)
      case Elem(element, randomVar) => false
      case Event(base, sort) => false
      case InIsle(isleVar, boat, isle) => varDepends(t)(isleVar)
      case PairEvent(base1, base2, sort) => false
    }

  def equationDepends(t: Term)(eq : Equation) : Boolean = {
    import Expression.varVals
    val genvars = varVals(eq.lhs).map(_.variable) union varVals(eq.lhs).map(_.variable)
    genvars.exists(v => varDepends(t)(v))
  }
Out[56]:
defined function varDepends
defined function equationDepends
In [57]:
ev0.equations.size
Out[57]:
res56: Int = 739
In [58]:
ev0.equations.take(20).map(equationDepends(a))
Out[58]:
res57: Set[Boolean] = Set(false, true)
In [59]:
ev0.equations.take(100).map(equationDepends(a))
Out[59]:
res58: Set[Boolean] = Set(false, true)
In [60]:
val indepEqs= ev0.equations.filterNot(equationDepends(a))
Out[60]:
indepEqs: Set[Equation] = Set(
  Equation(
    InitialVal(
      InIsle(
        Elem(A, Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar((B → A)), Sigma, EnterIsle)
      )
    ),
    Product(IsleScale(@a, Elem(A, Typs)), InitialVal(Elem(A, Typs)))
  ),
  Equation(
    InitialVal(
      InIsle(
        Elem(A, Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar((A → A)), Sigma, EnterIsle)
      )
    ),
    Product(IsleScale(@a, Elem(A, Typs)), InitialVal(Elem(A, Typs)))
  ),
  Equation(
    FinalVal(
      InIsle(
        InIsle(
          Elem(B, Typs),
          @b,
          Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
        ),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
      )
    ),
    Product(
      Coeff(Init(Typs)),
      InitialVal(
        InIsle(
          InIsle(
            Elem(B, Typs),
...

This was computed fast. The previous shortcut based attempt made things slow. For safety, we will run the update in a copy of this notebook.