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 [ ]: