When we have variables such as $A: Type$, $a : A$ and $B: Type$, we test whether we correctly:
This time the test is more refined. Namely,
In [1]:
import $cp.bin.`provingground-core-jvm-8dd937ec3a.fat.jar`
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
Out[1]:
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), context = Context.Empty.addVariable(A).addVariable(B).addVariable(a))
Out[2]:
In [3]:
val lp = LocalProver(ts)
Out[3]:
In [4]:
ts.vars
import TermData._
val datT = termData(lp)
Out[4]:
In [5]:
import monix.execution.Scheduler.Implicits.global
val td = datT.runSyncUnsafe()
Out[5]:
In [6]:
val (ns, eqs) = td
Out[6]:
In [7]:
val atoms = (eqs.map(_.rhs).flatMap(Expression.varVals(_)) union eqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[7]:
In [8]:
import TermRandomVars._, GeneratorVariables._
val elemTerms = atoms.collect{case Elem(t: Term, Terms) => t}
Out[8]:
In [9]:
elemTerms.exists(_.dependsOn(A))
Out[9]:
In [10]:
atoms.size
Out[10]:
In [11]:
val elemTyps = atoms.collect{case Elem(t: Typ[Term], Typs) => t}
Out[11]:
In [12]:
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))
Out[12]:
In [13]:
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[13]:
In [14]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}
Out[14]:
In [15]:
elemTerms == normElemTerms
Out[15]:
In [16]:
val ts0 = TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))
Out[16]:
In [17]:
val ev = ExpressionEval.fromInitEqs(ts0, Equation.group(eqs), TermGenParams(), decayS = 0.95)
Out[17]:
In [18]:
val termsT = ev.finalTerms
Out[18]:
In [19]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.95)
Out[19]:
In [20]:
val termsN = evN.finalTerms
Out[20]:
In [21]:
termsT.support == termsN.support
Out[21]:
In [22]:
ExpressionEval.mapRatio(termsT.toMap, termsN.toMap)
Out[22]:
In [23]:
val bigT = termsT.support.maxBy(t => termsT(t) / termsN(t))
Out[23]:
In [24]:
termsT(bigT)
termsN(bigT)
Out[24]:
In [25]:
val bigN = termsT.support.maxBy(t => termsN(t) / termsT(t))
Out[25]:
In [26]:
termsT(bigN)
termsN(bigN)
Out[26]:
In [27]:
val ns = lp.nextState.runSyncUnsafe()
Out[27]:
The error is clearly present here too. The next check is where we change the context.
In [28]:
val ts1 = ts.copy(context = Context.Empty)
Out[28]:
In [29]:
val lp1 = lp.copy(initState = ts1)
Out[29]:
In [30]:
val ns1 = lp1.nextState.runSyncUnsafe()
Out[30]:
In [31]:
ns1.terms.support -- ns.terms.support
Out[31]:
In [32]:
ns.terms.support -- ns1.terms.support
Out[32]:
In [33]:
val t = ns.terms.pmf(13).elem
Out[33]:
In [35]:
val tOpt = ns1.terms.support.find(x => x == t)
Out[35]:
In [36]:
tOpt.get == t
Out[36]:
In [37]:
t == tOpt.get
Out[37]:
In [38]:
val x = nextVar(A, Vector(A, B, a))
Out[38]:
In [39]:
val ctx = ts.context.addVariable(x)
val y = nextVar(A, ctx.variables)
Out[39]:
In [40]:
ts.context
Out[40]:
In [41]:
ts.context.variables
Out[41]:
In [42]:
ctx.variables
Out[42]:
It is evident what caused the error - the variable in a context changed its type. The code has been corrected to no longer use contexts, and the stuff should be run without contexts.