Testing export and normalization of isles

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

  • export equations, so that variables end up in islands
  • normalize isle names.
In [1]:
import $cp.bin.`provingground-core-jvm-7f2148cb82.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 ts = TermState(FiniteDistribution.empty, FiniteDistribution.unif(A, B), vars = Vector(A, B), context = Context.Empty.addVariable(A).addVariable(B))
Out[2]:
A: Typ[Term] = A
B: Typ[Term] = B
ts: TermState = TermState(
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
  Vector(A, B),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  AppendVariable(AppendVariable(Empty, A), B)
)
In [3]:
val lp = LocalProver(ts)
Out[3]:
lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
    Vector(A, B),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    AppendVariable(AppendVariable(Empty, A), B)
  ),
  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)
import TermData._

datT: monix.eval.Task[(TermState, Set[EquationNode])] = FlatMap(
  Async(<function2>, false, true, true),
  provingground.learning.TermData$$$Lambda$2568/1850628006@2c290d4f
)
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 : B) ā†¦ (@a : B) ā†¦ @a,
          0.02560842551463784
        ),
        Weighted(
          (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((```@a_1 , @a_2) : BƗA) ā†¦ (```@a_1 , @a_2),
          0.00485109621675388
        ),
        Weighted(
          (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((``@a_1 , @a_2) : AƗA) ā†¦ (``@a_1 , @a_2),
          0.00485109621675388
        ),
        Weighted(
          (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : ((B ā†’ A) ā†’ A)) ā†¦ @a,
          7.546149670506037E-4
        ),
        Weighted(
          (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : (A ā†’ A)) ā†¦ @a,
          0.009055379604607243
        ),
        Weighted(
          (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : (B ā†’ A)) ā†¦ @a,
          0.009055379604607243
        ),
        Weighted(
          (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : ((A ā†’ B) ā†’ A)) ā†¦ @a,
          7.546149670506037E-4
        ),
        Weighted(
          (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : ((B ā†’ B) ā†’ A)) ā†¦ @a,
          7.546149670506037E-4
        ),
        Weighted(
          (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : ((A ā†’ A) ā†’ A)) ā†¦ @a,
          7.546149670506037E-4
...
In [6]:
val (ns, eqs) = td
Out[6]:
ns: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(
        (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : B) ā†¦ (@a : B) ā†¦ @a,
        0.02560842551463784
      ),
      Weighted(
        (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((```@a_1 , @a_2) : BƗA) ā†¦ (```@a_1 , @a_2),
        0.00485109621675388
      ),
      Weighted(
        (A : š’° ) ā†¦ (B : š’° ) ā†¦ ((``@a_1 , @a_2) : AƗA) ā†¦ (``@a_1 , @a_2),
        0.00485109621675388
      ),
      Weighted(
        (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : ((B ā†’ A) ā†’ A)) ā†¦ @a,
        7.546149670506037E-4
      ),
      Weighted(
        (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : (A ā†’ A)) ā†¦ @a,
        0.009055379604607243
      ),
      Weighted(
        (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : (B ā†’ A)) ā†¦ @a,
        0.009055379604607243
      ),
      Weighted(
        (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : ((A ā†’ B) ā†’ A)) ā†¦ @a,
        7.546149670506037E-4
      ),
      Weighted(
        (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : ((B ā†’ B) ā†’ A)) ā†¦ @a,
        7.546149670506037E-4
      ),
      Weighted(
        (A : š’° ) ā†¦ (B : š’° ) ā†¦ (@a : ((A ā†’ A) ā†’ A)) ā†¦ @a,
        7.546149670506037E-4
      ),
...
eqs: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      InIsle(
        InIsle(
          Elem((@a : B) ā†¦ (@a : A) ā†¦ @a, Terms),
          B,
          Island(
            Terms,
            ConstRandVar(Terms),
            provingground.learning.ExpressionEval$$Lambda$2849/1630657925@311dc655,
            Lambda,
            EnterIsle
          )
        ),
        A,
        Island(
          Typs,
          ConstRandVar(Typs),
          provingground.learning.ExpressionEval$$Lambda$2843/36094366@65c43056,
          Pi,
          EnterIsle
        )
      )
    ),
    Product(
      Product(
        Coeff(
          BaseThenCondition(
            FlatMap(Typs, LambdaIsle, Terms),
            Funcs,
            Restrict(FuncOpt)
          )
        ),
        FinalVal(
          InIsle(
            InIsle(
              Elem(B, Typs),
...
In [7]:
ns.vars
Out[7]:
res6: Vector[Term] = Vector()
In [8]:
eqs.map(_.lhs)
Out[8]:
res7: Set[Expression] = Set(
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(A, Typs),
            @a,
            Island(Typs, ConstRandVar(Typs), AddVar(B, 0.3), Pi, EnterIsle)
          ),
          @a,
          Island(Typs, ConstRandVar(Typs), AddVar(A, 0.3), Pi, EnterIsle)
        ),
        B,
        Island(
          Terms,
          ConstRandVar(Terms),
          provingground.learning.ExpressionEval$$Lambda$2849/1630657925@311dc655,
          Lambda,
          EnterIsle
        )
      ),
      A,
      Island(
        Typs,
        ConstRandVar(Typs),
        provingground.learning.ExpressionEval$$Lambda$2843/36094366@65c43056,
        Pi,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(A, Typs),
...
In [9]:
eqs.map(_.rhs)
Out[9]:
res8: Set[Expression] = Set(
  Product(
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2477/1176821309@30bad48c,
          Typs
        )
      ),
      FinalVal(
        InIsle(
          InIsle(
            Elem(B, Typs),
            B,
            Island(
              Typs,
              ConstRandVar(Typs),
              provingground.learning.ExpressionEval$$Lambda$2843/36094366@55b6dcee,
              Pi,
              EnterIsle
            )
          ),
          A,
          Island(
            Terms,
            ConstRandVar(Terms),
            provingground.learning.ExpressionEval$$Lambda$2849/1630657925@46cccb02,
            Lambda,
            EnterIsle
          )
        )
      )
    ),
    FinalVal(
      InIsle(
...

First conclusion

After correction, variables seem to be in isles

In [10]:
eqs.map(_.rhs).flatMap(Expression.varVals(_))
Out[10]:
res9: Set[Expression.VarVal[_]] = Set(
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(A, Typs),
            @a,
            Island(Typs, ConstRandVar(Typs), AddVar(B, 0.3), Pi, EnterIsle)
          ),
          @a,
          Island(Typs, ConstRandVar(Typs), AddVar(A, 0.3), Pi, EnterIsle)
        ),
        B,
        Island(
          Terms,
          ConstRandVar(Terms),
          provingground.learning.ExpressionEval$$Lambda$2849/1630657925@311dc655,
          Lambda,
          EnterIsle
        )
      ),
      A,
      Island(
        Typs,
        ConstRandVar(Typs),
        provingground.learning.ExpressionEval$$Lambda$2843/36094366@65c43056,
        Pi,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(A, Typs),
...
In [11]:
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))
Out[11]:
normEqs: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      InIsle(
        Elem(āˆ(B : š’° ){ (@a ā†’ @a)ƗB }, Typs),
        @a,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@4276b616,
          AddVar(š’° , 0.3),
          Pi,
          EnterIsle
        )
      )
    ),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2476/1640843147@27417ca4,
          Typs
        )
      ),
      FinalVal(
        InIsle(
          InIsle(
            Elem((@a ā†’ @a)Ɨ@b, Typs),
            @b,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@58383e99,
              AddVar(š’° , 0.3),
              Pi,
              EnterIsle
            )
          ),
...
In [12]:
show(normEqs.take(10).map(_.rhs).flatMap(Expression.varVals(_)))

Set(
  FinalVal(
    InIsle(
      InIsle(
        Elem((@a : @b) ā†¦ (@a : @a) ā†¦ @a, Terms),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@ab64c0c,
          AddVar(š’° , 0.3),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@551dcf28,
        AddVar(š’° , 0.3),
        Lambda,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        Elem(
          Wrap((@a : (@b ā†’ @b)) ā†¦ @a),
          AtCoord(FuncsWithDomain, (@b ā†’ @b) :: HNil)
        ),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@61dcddb,
          AddVar(š’° , 0.3),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@6b3558bd,
        AddVar(š’° , 0.3),
        Lambda,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@a, Typs),
            @b,
            Island(
              Typs,
              provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@60925028,
              AddVar(@b, 0.3),
              Pi,
              EnterIsle
            )
          ),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@1753f1fe,
            AddVar(@b, 0.3),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@2f562610,
          AddVar(š’° , 0.3),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@383bde9a,
        AddVar(š’° , 0.3),
        Lambda,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        Elem((@a : @b) ā†¦ @a, Terms),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@147b4021,
          AddVar(š’° , 0.3),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@412838e9,
        AddVar(š’° , 0.3),
        Lambda,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        Elem((@a ā†’ @a)Ɨ@b, Typs),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@58383e99,
          AddVar(š’° , 0.3),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@6fc30148,
        AddVar(š’° , 0.3),
        Pi,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        Elem((@bƗ@b ā†’ @b), Typs),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@d54615a,
          AddVar(š’° , 0.3),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@5e755b40,
        AddVar(š’° , 0.3),
        Pi,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          Elem(@a, Terms),
          @a,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@3932df9e,
            AddVar(((@b ā†’ @a) ā†’ @b), 0.3),
            Lambda,
            EnterIsle
          )
        ),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@14b44755,
          AddVar(š’° , 0.3),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@12d88a3a,
        AddVar(š’° , 0.3),
        Pi,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          Elem(@a, Typs),
          @a,
          Island(
            Typs,
            provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@2630b406,
            AddVar((@b ā†’ @a), 0.3),
            Pi,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@20793225,
          AddVar(š’° , 0.3),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@7fb05632,
        AddVar(š’° , 0.3),
        Lambda,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        Event(
          Terms,
          Restrict(
            provingground.learning.TermRandomVars$$$Lambda$3039/1079830253@478afd5a
          )
        ),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@378769bf,
          AddVar(š’° , 0.3),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Terms,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@f69956f,
        AddVar(š’° , 0.3),
        Lambda,
        EnterIsle
      )
    )
  ),
  InitialVal(
    InIsle(
      InIsle(
        Elem(@a, Typs),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@1269d9a3,
          AddVar(š’° , 0.3),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@6d0dbae4,
        AddVar(š’° , 0.3),
        Pi,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        Elem(@bƗ@b, Typs),
        @b,
        Island(
          Terms,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@1893c0b4,
          AddVar(š’° , 0.3),
          Lambda,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@51cb90b5,
        AddVar(š’° , 0.3),
        Pi,
        EnterIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          Elem(Wrap((@a : @a) ā†¦ @a), Funcs),
          @a,
          Island(
            Terms,
            provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@2cad4880,
            AddVar(@b, 0.3),
            Lambda,
            EnterIsle
          )
        ),
        @b,
        Island(
          Typs,
          provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@46ca42b3,
          AddVar(š’° , 0.3),
          Pi,
          EnterIsle
        )
      ),
      @a,
      Island(
        Typs,
        provingground.learning.TermRandomVars$$$Lambda$3035/1581375871@620dd14a,
        AddVar(š’° , 0.3),
        Pi,
        EnterIsle
      )
    )
  )
)

Preliminary conclusion

The methods seem to work after a few rounds of debugging, in the sense that there are no visible errors.

In [ ]: