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-38c4a5770c.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$2550/1867903622@11402db7
)
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(
            InIsle(
              Elem(@a, Terms),
              @b,
              Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
            ),
            @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)
      )
    ),
    Product(
      Coeff(Init(Terms)),
      InitialVal(
        InIsle(
          InIsle(
            InIsle(
              InIsle(
                Elem(@a, Terms),
                @b,
                Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
              ),
              @a,
              Island(Typs, ConstRandVar(Typs), AddVar(A), Pi, EnterIsle)
            ),
            B,
            Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
          ),
          A,
...
In [7]:
val nonDetOpt = eqs.find(eq =>  TermData.isleNormalize(eq) != TermData.isleNormalize(eq))
Out[7]:
nonDetOpt: Option[EquationNode] = None
In [8]:
val atoms = (eqs.map(_.rhs).flatMap(Expression.varVals(_)) union eqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[8]:
atoms: Set[GeneratorVariables.Variable[Any]] = Set(
  InIsle(
    InIsle(
      InIsle(
        Elem((@b : B) ā†¦ @a, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(B), Lambda, EnterIsle)
      ),
      a,
      Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
    ),
    B,
    Island(Terms, ConstRandVar(Terms), AddVar(š’° ), Lambda, EnterIsle)
  ),
  InIsle(
    InIsle(
      Elem((@a : A) ā†¦ @a, Terms),
      B,
      Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
    ),
    A,
    Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
  ),
  InIsle(
    InIsle(
      InIsle(
        InIsle(
          Elem(A, Typs),
          @a,
          Island(Typs, ConstRandVar(Typs), AddVar(A), Pi, 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)
...
In [9]:
import TermRandomVars._, GeneratorVariables._
val elemTerms = atoms.collect{case Elem(t: Term, Terms) => t}
Out[9]:
import TermRandomVars._, GeneratorVariables._

elemTerms: 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 : 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) ā†¦ (@b : B) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : A) ā†¦ (@a : B) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : B) ā†¦ (@a : A) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : A) ā†¦ (@b : A) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : A) ā†¦ (@b : A) ā†¦ @b,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : A) ā†¦ (@b : A) ā†¦ a,
  (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 : (B ā†’ A)) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : (A ā†’ A)) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : (B ā†’ B)) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : (A ā†’ B)) ā†¦ @a,
  (B : š’° ) ā†¦ (@a : B) ā†¦ (@b : B) ā†¦ @b,
  (B : š’° ) ā†¦ (@a : B) ā†¦ (@b : B) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ B)) ā†¦ @a(a),
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ A)) ā†¦ @a(a),
  (B : š’° ) ā†¦ ((``@a_1 , @a_2) : BƗB) ā†¦ (``@a_1 , @a_2),
  (@a : B) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((``@a_1 , @a_2) : AƗA) ā†¦ (``@a_1 , @a_2),
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((```@a_1 , @a_2) : AƗB) ā†¦ (```@a_1 , @a_2),
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((``@a_1 , @a_2) : BƗB) ā†¦ (``@a_1 , @a_2),
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((```@a_1 , @a_2) : BƗA) ā†¦ (```@a_1 , @a_2),
  (A : š’° ) ā†¦ (a : A) ā†¦ A,
  (@a : (A ā†’ B)) ā†¦ a,
  (@a : (B ā†’ B)) ā†¦ a,
  (A : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ A)) ā†¦ @a,
  (@a : A) ā†¦ @a,
  (B : š’° ) ā†¦ B,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ A,
...
In [10]:
elemTerms.exists(_.dependsOn(A))
Out[10]:
res9: Boolean = true

First checks

  • None of the terms depends on the variables
  • The duplication in generated variables has stopped.
In [11]:
atoms.size
Out[11]:
res10: Int = 10020
In [12]:
val elemTyps = atoms.collect{case Elem(t: Typ[Term], Typs) => t}
Out[12]:
elemTyps: Set[Typ[Term]] = Set(
  A,
  āˆ(A : š’° ){ AƗAƗA },
  āˆ(B : š’° ){ BƗBƗB },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ BƗBƗB) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ BƗAƗA) } },
  āˆ(A : š’° ){ (š’°  ā†’ (A ā†’ AƗAƗA)) },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ AƗAƗB) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ AƗBƗB) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ BƗBƗA) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ AƗBƗA) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ BƗAƗB) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ AƗBƗB) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ BƗBƗB) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ AƗBƗA) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ BƗAƗA) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ BƗBƗA) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ AƗAƗB) } },
  āˆ(A : š’° ){ (š’°  ā†’ (A ā†’ AƗAƗA)) },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ BƗAƗB) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ (B ā†’ BƗB)) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ (A ā†’ BƗB)) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ (B ā†’ AƗA)) } },
  āˆ(A : š’° ){ (š’°  ā†’ (A ā†’ (A ā†’ AƗA))) },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ (B ā†’ AƗB)) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ (A ā†’ AƗB)) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ (B ā†’ BƗA)) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ (A ā†’ BƗA)) } },
  (š’°  ā†’ āˆ(B : š’° ){ (B ā†’ BƗB) }),
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ BƗB) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (B ā†’ BƗA) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ BƗA) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (B ā†’ AƗA) } },
  āˆ(A : š’° ){ (š’°  ā†’ (A ā†’ AƗA)) },
  āˆ(A : š’° ){ (A ā†’ (A ā†’ AƗA)) },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ AƗB) } },
  āˆ(A : š’° ){ āˆ(B : š’° ){ (B ā†’ AƗB) } },
  āˆ(B : š’° ){ (B ā†’ (B ā†’ B)) },
  (š’°  ā†’ āˆ(B : š’° ){ ((B ā†’ B) ā†’ B) }),
...
In [13]:
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))
Out[13]:
normEqs: Set[EquationNode] = Set(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              InIsle(
                Elem(@b, Terms),
                @b,
                Island(Typs, ConstRandVar(Typs), AddVar(@b), Pi, EnterIsle)
              ),
              @a,
              Island(Typs, ConstRandVar(Typs), AddVar(@b), Pi, EnterIsle)
            ),
            @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)
      )
    ),
    Product(IsleScale(%boat, Elem(%boat, Terms)), Literal(-1.0))
  ),
  EquationNode(
    FinalVal(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem(@a, Terms),
              @c,
              Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
            ),
            @b,
            Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
...
In [14]:
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[14]:
normAtoms: Set[Variable[Any]] = Set(
  InIsle(
    InIsle(
      InIsle(
        InIsle(
          Elem(@b, Typs),
          @b,
          Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
        ),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(@a), Sigma, EnterIsle)
      ),
      @b,
      Island(Terms, ConstRandVar(Terms), AddVar(š’° ), Lambda, EnterIsle)
    ),
    @a,
    Island(Terms, ConstRandVar(Terms), AddVar(š’° ), Lambda, 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((@a ā†’ (@b ā†’ @a)), Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
      ),
      @b,
...
In [15]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}
Out[15]:
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 : 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 : A) ā†¦ (@b : 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 : B) ā†¦ (@b : B) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : A) ā†¦ (@a : B) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : B) ā†¦ (@a : A) ā†¦ @a,
  (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 : (B ā†’ B)) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : (A ā†’ B)) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : (B ā†’ A)) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : (A ā†’ A)) ā†¦ @a,
  (B : š’° ) ā†¦ (@a : B) ā†¦ (@b : B) ā†¦ @b,
  (B : š’° ) ā†¦ (@a : B) ā†¦ (@b : B) ā†¦ @a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ A)) ā†¦ @a(a),
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ B)) ā†¦ @a(a),
  (B : š’° ) ā†¦ ((``@a_1 , @a_2) : BƗB) ā†¦ (``@a_1 , @a_2),
  (@a : B) ā†¦ a,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((``@a_1 , @a_2) : AƗA) ā†¦ (``@a_1 , @a_2),
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((``@a_1 , @a_2) : BƗB) ā†¦ (``@a_1 , @a_2),
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((```@a_1 , @a_2) : AƗB) ā†¦ (```@a_1 , @a_2),
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((```@a_1 , @a_2) : BƗA) ā†¦ (```@a_1 , @a_2),
  (A : š’° ) ā†¦ (a : A) ā†¦ A,
  (@a : (A ā†’ B)) ā†¦ a,
  (@a : (B ā†’ B)) ā†¦ a,
  (A : š’° ) ā†¦ (a : A) ā†¦ (@a : (A ā†’ A)) ā†¦ @a,
  (@a : A) ā†¦ @a,
  (B : š’° ) ā†¦ B,
  (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ B,
...
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@4cec84b3
In [19]:
val termsT = ev.finalTerms
Out[19]:
termsT: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      (A : š’° ) ā†¦ (a : A) ā†¦ (@a : A) ā†¦ (@b : A) ā†¦ @a,
      9.276485722945591E-4
    ),
    Weighted(
      (A : š’° ) ā†¦ (a : A) ā†¦ (@a : A) ā†¦ (@b : A) ā†¦ @b,
      0.001325217461338344
    ),
    Weighted(
      (A : š’° ) ā†¦ (a : A) ā†¦ (@a : A) ā†¦ (@b : A) ā†¦ a,
      6.551449356602914E-4
    ),
    Weighted(
      (A : š’° ) ā†¦ (a : A) ā†¦ ((``@a_1 , @a_2) : AƗA) ā†¦ (``@a_1 , @a_2),
      0.006482343732652738
    ),
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((```@a_1 , @a_2) : AƗB) ā†¦ (```@a_1 , @a_2),
      6.482328556913037E-4
    ),
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((``@a_1 , @a_2) : BƗB) ā†¦ (``@a_1 , @a_2),
      6.482334239667172E-4
    ),
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((```@a_1 , @a_2) : BƗA) ā†¦ (```@a_1 , @a_2),
      6.481468665912907E-4
    ),
    Weighted(
      (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ ((``@a_1 , @a_2) : AƗA) ā†¦ (``@a_1 , @a_2),
      6.481464725181117E-4
    ),
    Weighted(
...
In [20]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.95)
Out[20]:
evN: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@173e151
In [20]:
// val termsN = evN.finalTerms
In [21]:
import ExpressionEval._
Out[21]:
import ExpressionEval._
In [22]:
val m1 = nextMap(evN.init, evN.equations)
Out[22]:
m1: Map[Expression, Double] = Map(
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@a, Terms),
            @a,
            Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
          ),
          @a,
          Island(Typs, ConstRandVar(Typs), AddVar(@b), Pi, EnterIsle)
        ),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(š’° ), Lambda, EnterIsle)
      ),
      @a,
      Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
    )
  ) -> 0.30000000000000004,
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem(@b, Terms),
              @b,
              Island(
                AtCoord(FuncsWithDomain, @a :: HNil),
                ConstRandVar(Terms),
                AddVar(@a),
                Lambda,
                EnterIsle
              )
            ),
            @a,
            Island(Terms, ConstRandVar(Terms), AddVar(@b), Lambda, EnterIsle)
          ),
...
In [23]:
m1.values
Out[23]:
res22: Iterable[Double] = MapLike.DefaultValuesIterable(
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.1,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.7,
  0.30000000000000004,
  0.7,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.7,
  0.7,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
  0.1,
  0.30000000000000004,
  0.30000000000000004,
  0.30000000000000004,
...
In [24]:
val exp = m1.find(_._2 < 0).get._1
Out[24]:
exp: Expression = InitialVal(
  InIsle(
    InIsle(
      Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
    ),
    @a,
    Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
  )
)
In [25]:
val rhs = evN.equations.find(_.lhs == exp).map(_.rhs).get
Out[25]:
rhs: Expression = Sum(
  Sum(
    Literal(1.0),
    Product(
      IsleScale(%boat, Elem(%boat, AtCoord(TermsWithTyp, A :: HNil))),
      Literal(-1.0)
    )
  ),
  Product(
    IsleScale(%boat, Elem(%boat, AtCoord(TermsWithTyp, B :: HNil))),
    Literal(-1.0)
  )
)
In [26]:
normEqs.filter(_.lhs == exp)
Out[26]:
res25: Set[EquationNode] = Set(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
      )
    ),
    Literal(1.0)
  ),
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
      )
    ),
    Product(
      IsleScale(%boat, Elem(%boat, AtCoord(TermsWithTyp, B :: HNil))),
      Literal(-1.0)
    )
  ),
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
...
In [27]:
normEqs.filter(_.lhs == exp).size
Out[27]:
res26: Int = 3
In [28]:
val baseEqs = eqs.filter(eq => TermData.isleNormalize(eq).lhs == exp)
Out[28]:
baseEqs: Set[EquationNode] = Set(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(a, AtCoord(TermsWithTyp, A :: HNil)),
          a,
          Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
        ),
        A,
        Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
      )
    ),
    Literal(1.0)
  ),
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, AtCoord(TermsWithTyp, B :: HNil)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(B), Lambda, EnterIsle)
        ),
        B,
        Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
      )
    ),
    Product(
      IsleScale(@a, Elem(@a, AtCoord(TermsWithTyp, B :: HNil))),
      Literal(-1.0)
    )
  ),
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(a, AtCoord(TermsWithTyp, A :: HNil)),
          a,
          Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
...
In [29]:
baseEqs.size
Out[29]:
res28: Int = 6
In [30]:
show(baseEqs.map(_.rhs))

Set(
  Product(
    IsleScale(a, Elem(a, AtCoord(TermsWithTyp, A :: HNil))),
    Literal(-1.0)
  ),
  Product(
    IsleScale(@a, Elem(@a, AtCoord(TermsWithTyp, B :: HNil))),
    Literal(-1.0)
  ),
  Product(
    IsleScale(@a, Elem(@a, AtCoord(TermsWithTyp, A :: HNil))),
    Literal(-1.0)
  ),
  Literal(1.0)
)
In [31]:
show(baseEqs.map(_.lhs))

Set(
  InitialVal(
    InIsle(
      InIsle(
        Elem(a, AtCoord(TermsWithTyp, A :: HNil)),
        a,
        Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
      ),
      A,
      Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
    )
  ),
  InitialVal(
    InIsle(
      InIsle(
        Elem(@a, AtCoord(TermsWithTyp, B :: HNil)),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(B), Lambda, EnterIsle)
      ),
      B,
      Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
    )
  ),
  InitialVal(
    InIsle(
      InIsle(
        Elem(@a, AtCoord(TermsWithTyp, A :: HNil)),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
      ),
      A,
      Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
    )
  )
)
In [32]:
show(normEqs.filter(_.lhs == exp))

Set(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
      )
    ),
    Literal(1.0)
  ),
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
      )
    ),
    Product(
      IsleScale(%boat, Elem(%boat, AtCoord(TermsWithTyp, B :: HNil))),
      Literal(-1.0)
    )
  ),
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
      )
    ),
    Product(
      IsleScale(%boat, Elem(%boat, AtCoord(TermsWithTyp, A :: HNil))),
      Literal(-1.0)
    )
  )
)
In [33]:
val baseGps = baseEqs.groupBy(eq => TermData.isleNormalize(eq))
Out[33]:
baseGps: Map[EquationNode, Set[EquationNode]] = Map(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
      )
    ),
    Literal(1.0)
  ) -> Set(
    EquationNode(
      InitialVal(
        InIsle(
          InIsle(
            Elem(a, AtCoord(TermsWithTyp, A :: HNil)),
            a,
            Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
          ),
          A,
          Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
        )
      ),
      Literal(1.0)
    ),
    EquationNode(
      InitialVal(
        InIsle(
          InIsle(
            Elem(@a, AtCoord(TermsWithTyp, B :: HNil)),
            @a,
            Island(Terms, ConstRandVar(Terms), AddVar(B), Lambda, EnterIsle)
          ),
          B,
          Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
...
In [34]:
show(baseGps.head)

(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
      )
    ),
    Literal(1.0)
  ),
  Set(
    EquationNode(
      InitialVal(
        InIsle(
          InIsle(
            Elem(a, AtCoord(TermsWithTyp, A :: HNil)),
            a,
            Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
          ),
          A,
          Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
        )
      ),
      Literal(1.0)
    ),
    EquationNode(
      InitialVal(
        InIsle(
          InIsle(
            Elem(@a, AtCoord(TermsWithTyp, B :: HNil)),
            @a,
            Island(Terms, ConstRandVar(Terms), AddVar(B), Lambda, EnterIsle)
          ),
          B,
          Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
        )
      ),
      Literal(1.0)
    ),
    EquationNode(
      InitialVal(
        InIsle(
          InIsle(
            Elem(@a, AtCoord(TermsWithTyp, A :: HNil)),
            @a,
            Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
          ),
          A,
          Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
        )
      ),
      Literal(1.0)
    )
  )
)
In [35]:
baseGps.head._2.size
Out[35]:
res34: Int = 3
In [36]:
baseGps.size
Out[36]:
res35: Int = 3
In [37]:
baseGps.values.map(_.size)
Out[37]:
res36: Iterable[Int] = List(3, 2, 1)
In [38]:
show(baseGps.tail.head)

(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
      )
    ),
    Product(
      IsleScale(%boat, Elem(%boat, AtCoord(TermsWithTyp, A :: HNil))),
      Literal(-1.0)
    )
  ),
  Set(
    EquationNode(
      InitialVal(
        InIsle(
          InIsle(
            Elem(a, AtCoord(TermsWithTyp, A :: HNil)),
            a,
            Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
          ),
          A,
          Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
        )
      ),
      Product(
        IsleScale(a, Elem(a, AtCoord(TermsWithTyp, A :: HNil))),
        Literal(-1.0)
      )
    ),
    EquationNode(
      InitialVal(
        InIsle(
          InIsle(
            Elem(@a, AtCoord(TermsWithTyp, A :: HNil)),
            @a,
            Island(Terms, ConstRandVar(Terms), AddVar(A), Lambda, EnterIsle)
          ),
          A,
          Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
        )
      ),
      Product(
        IsleScale(@a, Elem(@a, AtCoord(TermsWithTyp, A :: HNil))),
        Literal(-1.0)
      )
    )
  )
)
In [39]:
show(baseGps.tail.tail.head)

(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
        ),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
      )
    ),
    Product(
      IsleScale(%boat, Elem(%boat, AtCoord(TermsWithTyp, B :: HNil))),
      Literal(-1.0)
    )
  ),
  Set(
    EquationNode(
      InitialVal(
        InIsle(
          InIsle(
            Elem(@a, AtCoord(TermsWithTyp, B :: HNil)),
            @a,
            Island(Terms, ConstRandVar(Terms), AddVar(B), Lambda, EnterIsle)
          ),
          B,
          Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
        )
      ),
      Product(
        IsleScale(@a, Elem(@a, AtCoord(TermsWithTyp, B :: HNil))),
        Literal(-1.0)
      )
    )
  )
)
In [40]:
import TermRandomVars._, TermGeneratorNodes._
val rvA = termsWithTyp(A)
Out[40]:
import TermRandomVars._, TermGeneratorNodes._

rvA: RandomVar[Term] = AtCoord(TermsWithTyp, A :: HNil)
In [41]:
randomVarSubs(A, B)(rvA)
Out[41]:
res40: RandomVar[Term] = AtCoord(TermsWithTyp, B :: HNil)
In [43]:
val eqn = baseGps.toVector(2)._2.head
Out[43]:
eqn: EquationNode = EquationNode(
  InitialVal(
    InIsle(
      InIsle(
        Elem(@a, AtCoord(TermsWithTyp, B :: HNil)),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(B), Lambda, EnterIsle)
      ),
      B,
      Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
    )
  ),
  Product(
    IsleScale(@a, Elem(@a, AtCoord(TermsWithTyp, B :: HNil))),
    Literal(-1.0)
  )
)
In [44]:
TermData.isleNormalize(eqn)
Out[44]:
res43: EquationNode = EquationNode(
  InitialVal(
    InIsle(
      InIsle(
        Elem(@a, AtCoord(TermsWithTyp, @a :: HNil)),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(@a), Lambda, EnterIsle)
      ),
      @a,
      Island(Typs, ConstRandVar(Typs), AddVar(š’° ), Pi, EnterIsle)
    )
  ),
  Product(
    IsleScale(%boat, Elem(%boat, AtCoord(TermsWithTyp, B :: HNil))),
    Literal(-1.0)
  )
)

New bug identification

  • The step when @a got replaced with %boat, both of type B, is fine.
  • However, when B got replaced by @a, we should have had a change in the random variable.
  • The fundamental problem is that the lhs and rhs are treated independently, but should not be.