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-9fbe6a3410.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$2573/1171249675@2e85f69b
)

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 : (B → B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → 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]:
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))


Out[11]:
normEqs: Set[EquationNode] = Set(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              InIsle(
                Elem(@b, Terms),
                @c,
                Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
              ),
              @b,
              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)
      )
    ),
    Product(
      IsleScale(%boat, Elem(@b, Terms)),
      InitialVal(
        InIsle(
          InIsle(
            InIsle(
              InIsle(
                Elem(@b, Terms),
                @b,
                Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
              ),
              @a,
              Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
            ),
...

In [12]:
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)


Out[12]:
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((@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)
  ),
  InIsle(
    InIsle(
      InIsle(
        Elem((@b → (@a → @a)), Typs),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
      ),
      @b,
...

In [13]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}


Out[13]:
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 : (B → B)) ↦ a,
  (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : (A → 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 [14]:
elemTerms == normElemTerms


Out[14]:
res13: Boolean = true

Next conclusion

  • terms are generated correctly
  • however, this does not test deeper generation, for which we must generate with the equations.

In [15]:
val ts0 = TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))


Out[15]:
ts0: TermState = TermState(
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)

In [16]:
val ev = ExpressionEval.fromInitEqs(ts0, Equation.group(eqs), TermGenParams(), decayS = 0.95)


Out[16]:
ev: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@42a9c46

In [17]:
val termsT = ev.finalTerms


Out[17]:
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 [18]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.95)


Out[18]:
evN: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@314b1c03

In [18]:
// val termsN = evN.finalTerms

In [19]:
evN.init


Out[19]:
res18: Map[Expression, Double] = Map(
  Coeff(
    BaseThenCondition(
      FiberProductMap(domOf, TermsWithTyp, Appln, TypFamilies, Terms),
      Typs,
      Restrict(TypOpt)
    )
  ) -> 0.1,
  IsleScale(%boat, Elem(Wrap(@a), Funcs)) -> 0.7,
  IsleScale(%boat, Elem(Wrap(@a), Funcs)) -> 0.7,
  IsleScale(%boat, Elem(Wrap(@a), Funcs)) -> 0.7,
  IsleScale(%boat, Elem(@a, Typs)) -> 0.7,
  IsleScale(%boat, Elem(@a, Typs)) -> 0.7,
  IsleScale(%boat, Elem(@a, Typs)) -> 0.7,
  IsleScale(%boat, Elem(@a, Typs)) -> 0.7,
  IsleScale(%boat, Elem(@a, Typs)) -> 0.7,
  IsleScale(%boat, Elem(@a, Typs)) -> 0.7,
  Coeff(
    BaseThenCondition(
      FiberProductMap(typeOf(_), FuncsWithDomain, FlipAppn, Terms, Terms),
      AtCoord(FuncsWithDomain, A :: HNil),
      Restrict(FuncWithDom(A))
    )
  ) -> 0.1,
  IsleScale((%boat_1 , %boat_2), Elem(@b, Typs)) -> 0.7,
  InitialVal(Elem(Wrap(@a), Funcs)) -> 0.4285714285714286,
  InitialVal(Elem(Wrap(@a), Funcs)) -> 0.4285714285714286,
  InitialVal(Elem(Wrap(@a), Funcs)) -> 0.4285714285714286,
  IsleScale(%boat, Elem(@a, Typs)) -> 0.7,
  IsleScale((%boat_1 , %boat_2), Elem(@a, Typs)) -> 0.7,
  Coeff(
    Island(
      AtCoord(FuncsWithDomain, (B → A) :: HNil),
      ConstRandVar(Terms),
      AddVar((B → A)),
      Lambda,
      EnterIsle
    )
  ) -> 0.1,
...

In [20]:
import ExpressionEval._


Out[20]:
import ExpressionEval._

In [21]:
evN.equations


Out[21]:
res20: Set[Equation] = Set(
  Equation(
    InitialVal(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              InIsle(
                Elem(@b, Terms),
                @c,
                Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
              ),
              @b,
              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)
      )
    ),
    Product(
      IsleScale(%boat, Elem(@b, Terms)),
      InitialVal(
        InIsle(
          InIsle(
            InIsle(
              InIsle(
                Elem(@b, Terms),
                @b,
                Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
              ),
              @a,
              Island(Typs, ConstRandVar(Typs), AddVar(@a), Pi, EnterIsle)
            ),
...

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]:
val exp = m1.find(_._2 < 0)


Out[23]:
exp: Option[(Expression, Double)] = None

Another bug fixed

Now we do not get negative values. We should check for evolution.


In [24]:
val termsN = evN.finalTerms


Out[24]:
termsN: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      (A : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@b : A) ↦ @a,
      0.004532899537709898
    ),
    Weighted(
      (A : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@b : A) ↦ a,
      0.004532899537709898
    ),
    Weighted(
      (A : 𝒰 ) ↦ (a : A) ↦ (@a : A) ↦ (@b : A) ↦ @b,
      0.003511936190810092
    ),
    Weighted(
      (A : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×A) ↦ (``@a_1 , @a_2),
      0.010111698689923442
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : A×B) ↦ (```@a_1 , @a_2),
      0.0010111674867781808
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : A×A) ↦ (``@a_1 , @a_2),
      0.0010110327385271037
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((```@a_1 , @a_2) : B×A) ↦ (```@a_1 , @a_2),
      0.0010110333538880852
    ),
    Weighted(
      (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ ((``@a_1 , @a_2) : B×B) ↦ (``@a_1 , @a_2),
      0.0010111683741543902
    ),
    Weighted(
...

In [25]:
evN.finalDist


Out[25]:
res24: 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.3000000000000001,
  FinalVal(
    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.16500000000000004,
...

In [26]:
evN.finalDist.keys


Out[26]:
res25: Iterable[Expression] = Set(
  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)
    )
  ),
  FinalVal(
    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)
    )
  ),
...

In [27]:
import Expression._
evN.finalDist.get(FinalVal(Elem(Type, Typs)))


Out[27]:
import Expression._

res26_1: Option[Double] = None

In [28]:
normEqs.filter(_.lhs == FinalVal(Elem(Type, Typs)))


Out[28]:
res27: Set[EquationNode] = Set()

In [29]:
eqs.filter(_.lhs == FinalVal(Elem(Type, Typs)))


Out[29]:
res28: Set[EquationNode] = Set()

In [30]:
ev.finalDist.get(FinalVal(Elem(Type, Typs)))


Out[30]:
res29: Option[Double] = None

In [31]:
val t = termsT.support.head


Out[31]:
t: Term = (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ a

In [32]:
eqs.find(_.lhs == Elem(t, Terms))


Out[32]:
res31: Option[EquationNode] = None

In [33]:
eqs.collect{case eqq @ EquationNode(FinalVal(Elem(_, _)), _) => eqq}


Out[33]:
res32: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(Elem(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → (A → B)) } }, Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2480/975632909@6b79a2f8,
          Typs
        )
      ),
      FinalVal(
        InIsle(
          Elem(∏(B : 𝒰 ){ (A → (A → B)) }, Typs),
          A,
          Island(Typs, ConstRandVar(Typs), AddVar(𝒰 ), Pi, EnterIsle)
        )
      )
    )
  ),
  EquationNode(
    FinalVal(Elem(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → (B → B)) } }, Typs)),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$2480/975632909@6b79a2f8,
          Typs
        )
      ),
      FinalVal(
        InIsle(
          Elem(∏(B : 𝒰 ){ (A → (B → B)) }, Typs),
          A,
          Island(Typs, ConstRandVar(Typs), AddVar(𝒰 ), Pi, EnterIsle)
        )
      )
...

In [34]:
val eqn0 = eqs.find(_.lhs == FinalVal(Elem(t, Terms))).get


Out[34]:
eqn0: EquationNode = EquationNode(
  FinalVal(
    Elem((A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ a, Terms)
  ),
  Product(
    Coeff(FlatMap(Typs, LambdaIsle, Terms)),
    FinalVal(
      InIsle(
        Elem((B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ a, Terms),
        A,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      )
    )
  )
)

In [35]:
TermRandomVars.isleNormalize(eqn0)


Out[35]:
res34: EquationNode = EquationNode(
  FinalVal(
    Elem((A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ a, Terms)
  ),
  Product(
    Coeff(FlatMap(Typs, LambdaIsle, Terms)),
    FinalVal(
      InIsle(
        Elem((B : 𝒰 ) ↦ (a : @a) ↦ (@a : B) ↦ (@a : @a) ↦ a, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      )
    )
  )
)

In [36]:
val rhs0 = varVals(eqn0.rhs).head


Out[36]:
rhs0: VarVal[Any] = FinalVal(
  InIsle(
    Elem((B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ a, Terms),
    A,
    Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
  )
)

In [37]:
ev.finalDist.get(rhs0)


Out[37]:
res36: Option[Double] = Some(1.659002455417805E-5)

In [38]:
val eqn1 = eqs.filter(_.lhs == rhs0).head


Out[38]:
eqn1: EquationNode = EquationNode(
  FinalVal(
    InIsle(
      Elem((B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ a, Terms),
      A,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
    )
  ),
  Product(
    Coeff(FlatMap(Typs, LambdaIsle, Terms)),
    FinalVal(
      InIsle(
        InIsle(
          Elem((a : A) ↦ (@a : B) ↦ (@a : A) ↦ a, Terms),
          B,
          Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
        ),
        A,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      )
    )
  )
)

In [39]:
import TermRandomVars._
isleNormalize(eqn1)


Out[39]:
import TermRandomVars._

res38_1: EquationNode = EquationNode(
  FinalVal(
    InIsle(
      Elem((B : 𝒰 ) ↦ (a : @a) ↦ (@a : B) ↦ (@a : @a) ↦ a, Terms),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
    )
  ),
  Product(
    Coeff(FlatMap(Typs, LambdaIsle, Terms)),
    FinalVal(
      InIsle(
        InIsle(
          Elem((a : @a) ↦ (@a : @b) ↦ (@a : @a) ↦ a, Terms),
          @b,
          Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
        ),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      )
    )
  )
)

In [40]:
normEqs.filter(_.lhs == FinalVal(Elem(t, Terms)))


Out[40]:
res39: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      Elem((A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (@a : B) ↦ (@a : A) ↦ a, Terms)
    ),
    Product(
      Coeff(FlatMap(Typs, LambdaIsle, Terms)),
      FinalVal(
        InIsle(
          Elem((B : 𝒰 ) ↦ (a : @a) ↦ (@a : B) ↦ (@a : @a) ↦ a, Terms),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
        )
      )
    )
  )
)

There is still an equation at this stage. May not be one at the next stage.


In [41]:
val rhsN= varVals(normEqs.filter(_.lhs == FinalVal(Elem(t, Terms))).head.rhs).head


Out[41]:
rhsN: VarVal[Any] = FinalVal(
  InIsle(
    Elem((B : 𝒰 ) ↦ (a : @a) ↦ (@a : B) ↦ (@a : @a) ↦ a, Terms),
    @a,
    Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
  )
)

Next bug: inconsistent normalization

  • Because there was no island on the left hand side, there was no normalization done to the rhs.
  • However when this appears on the lhs, there will be normalization.
  • Fix tried : in addition to substitution for the new expression, we should normalize.
  • partial effect: the island was modifieb, but terms still had 0 weight.

In [42]:
normEqs.filter(_.lhs == rhsN)


Out[42]:
res41: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      InIsle(
        Elem((B : 𝒰 ) ↦ (a : @a) ↦ (@a : B) ↦ (@a : @a) ↦ a, Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      )
    ),
    Product(
      Coeff(FlatMap(Typs, LambdaIsle, Terms)),
      FinalVal(
        InIsle(
          InIsle(
            Elem((a : @a) ↦ (@a : @b) ↦ (@a : @a) ↦ a, Terms),
            @b,
            Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
          ),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
        )
      )
    )
  )
)

In [43]:
isleNormalize(eqn1).rhs


Out[43]:
res42: Expression = Product(
  Coeff(FlatMap(Typs, LambdaIsle, Terms)),
  FinalVal(
    InIsle(
      InIsle(
        Elem((a : @a) ↦ (@a : @b) ↦ (@a : @a) ↦ a, Terms),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
    )
  )
)

In [44]:
rhsN


Out[44]:
res43: VarVal[Any] = FinalVal(
  InIsle(
    Elem((B : 𝒰 ) ↦ (a : @a) ↦ (@a : B) ↦ (@a : @a) ↦ a, Terms),
    @a,
    Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
  )
)

In [45]:
isleNormalize(eqn1).lhs


Out[45]:
res44: Expression = FinalVal(
  InIsle(
    Elem((B : 𝒰 ) ↦ (a : @a) ↦ (@a : B) ↦ (@a : @a) ↦ a, Terms),
    @a,
    Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
  )
)

In [46]:
val rhsN2 = varVals((normEqs.filter(_.lhs == rhsN)).head.rhs).head


Out[46]:
rhsN2: VarVal[Any] = FinalVal(
  InIsle(
    InIsle(
      Elem((a : @a) ↦ (@a : @b) ↦ (@a : @a) ↦ a, Terms),
      @b,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
    ),
    @a,
    Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
  )
)

In [47]:
normEqs.filter(_.lhs == rhsN2)


Out[47]:
res46: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      InIsle(
        InIsle(
          Elem((a : @a) ↦ (@a : @b) ↦ (@a : @a) ↦ a, Terms),
          @b,
          Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
        ),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      )
    ),
    Product(
      Coeff(FlatMap(Typs, LambdaIsle, Terms)),
      FinalVal(
        InIsle(
          InIsle(
            InIsle(
              Elem((@a : @b) ↦ (@a : @a) ↦ @a, Terms),
              @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)
        )
      )
    )
  )
)

In [48]:
val rhs2 = varVals((eqs.filter(_.lhs == rhs0)).head.rhs).head


Out[48]:
rhs2: VarVal[Any] = FinalVal(
  InIsle(
    InIsle(
      Elem((a : A) ↦ (@a : B) ↦ (@a : A) ↦ a, Terms),
      B,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
    ),
    A,
    Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
  )
)

In [49]:
eqs.filter(_.lhs == rhs2)


Out[49]:
res48: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      InIsle(
        InIsle(
          Elem((a : A) ↦ (@a : B) ↦ (@a : A) ↦ a, Terms),
          B,
          Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
        ),
        A,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 ), Lambda, EnterIsle)
      )
    ),
    Product(
      Coeff(FlatMap(Typs, LambdaIsle, Terms)),
      FinalVal(
        InIsle(
          InIsle(
            InIsle(
              Elem((@a : B) ↦ (@a : A) ↦ a, Terms),
              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)
        )
      )
    )
  )
)

More bug fixing

  • The missing terms bug is fixed.

In [50]:
ev.finalTerms.support -- termsT.support


Out[50]:
res49: Set[Term] = Set()

In [51]:
ev.finalTerms.support == termsT.support


Out[51]:
res50: Boolean = true

In [52]:
ExpressionEval.mapRatio(ev.finalTerms.toMap, termsT.toMap)


Out[52]:
res51: Double = 1.0

In [53]:
evN.finalTyps.support


Out[53]:
res52: Set[Typ[Term]] = Set(
  ∏(B : 𝒰 ){ B×B×B },
  ∏(A : 𝒰 ){ A×A×A },
  ∏(A : 𝒰 ){ (𝒰  → (A → A×A×A)) },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → B×B×B) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → B×A×B) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → A×A×B) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → B×A×A) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → B×B×A) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → A×B×B) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → A×B×A) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → A×A×B) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → B×B×B) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → B×A×B) } },
  ∏(A : 𝒰 ){ (𝒰  → (A → A×A×A)) },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → A×B×A) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → A×B×B) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → B×A×A) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → B×B×A) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → (B → B×A)) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → (B → A×A)) } },
  ∏(A : 𝒰 ){ (𝒰  → (A → (A → A×A))) },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → (A → B×A)) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → (B → B×B)) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → (A → B×B)) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → (A → A×B)) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → (B → A×B)) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (B → B×A) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (B → A×A) } },
  (𝒰  → ∏(B : 𝒰 ){ (B → B×B) }),
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (B → A×B) } },
  ∏(A : 𝒰 ){ (𝒰  → (A → A×A)) },
  ∏(A : 𝒰 ){ (A → (A → A×A)) },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → A×B) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → B×B) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → B×A) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (((A → A) → B) → A) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (((B → A) → B) → A) } },
  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ ((A → A) → B) } },
...

In [ ]:


In [ ]: