This is a simplified version, by raising cutoffs and sharpening decays.
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-b17f79ea57.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 normEqs = eqs.map(eq => TermData.isleNormalize(eq))
Out[11]:
In [12]:
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[12]:
In [13]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}
Out[13]:
In [14]:
elemTerms == normElemTerms
Out[14]:
In [15]:
val ts0 = TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))
Out[15]:
In [16]:
val ev = ExpressionEval.fromInitEqs(ts0, Equation.group(eqs), TermGenParams(), decayS = 0.75)
Out[16]:
In [17]:
val termsEv = ev.finalTerms
Out[17]:
In [18]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.75)
Out[18]:
In [19]:
val termsN = evN.finalTerms
Out[19]:
In [20]:
evN.init
Out[20]:
In [21]:
evN.maxRatio
Out[21]:
In [22]:
evN.decay
Out[22]:
In [23]:
evN.equations
Out[23]:
In [24]:
import ExpressionEval._
Out[24]:
In [25]:
val newMap = nextMap(evN.init, evN.equations, 0.5)
Out[25]:
In [26]:
val ss : Stream[Map[Expression, Double]] = evN.init #:: ss.map(m => nextMap(m, evN.equations, 0.5))
Out[26]:
In [27]:
val sizes = ss.map(_.keySet.size)
Out[27]:
In [28]:
sizes(2)
Out[28]:
In [29]:
sizes.take(20).toVector
Out[29]:
In [30]:
val stable= ss.zip(ss.tail).map{case (m1, m2) => m1.keySet == m2.keySet}
Out[30]:
In [31]:
stable.take(20).toVector
Out[31]:
In [32]:
val ratios = ss.tail.zip(ss.tail.tail).map{case (m1, m2) => mapRatio(m1, m2)}
Out[32]:
In [33]:
ratios.take(20).toVector
Out[33]:
In [34]:
val zeroes = ss.map(_.filter(_._2 == 0))
Out[34]:
In [35]:
zeroes.take(20).toVector
Out[35]:
In [36]:
val m1 = ss(1)
val m2 = ss(2)
Out[36]:
In [37]:
mapRatio(m1, m2)
Out[37]:
In [38]:
val triple = m1.map{case (k, v) => (k, v, m2(k))}
Out[38]:
In [39]:
triple.filter(t => t._2 == 0 || t._3 == 0)
Out[39]:
In [40]:
val rt = triple.map(t => (t._2/t._3, t._3/ t._2))
Out[40]:
In [41]:
triple.head._2
triple.head._3
Out[41]:
In [42]:
triple.map(_._3)
Out[42]:
In [43]:
triple.filterNot(_._3 < 2)
Out[43]:
In [44]:
m1.values.toSet
Out[44]:
In [45]:
m2.values.toSet
Out[45]:
In [46]:
val steps = normEqs.map(eq => recExp(m1, eq.rhs) -> eq)
Out[46]:
In [47]:
steps.map(_._1)
Out[47]:
In [48]:
val neg = steps.find(_._1 < 0)
Out[48]:
In [49]:
neg.get._2.rhs
Out[49]:
In [51]:
val source = eqs.find(eq => TermData.isleNormalize(eq) == neg.get)
Out[51]:
In [52]:
val source = eqs.filter(eq => TermData.isleNormalize(eq).lhs == neg.get._2.lhs)
Out[52]:
In [53]:
normEqs.contains(neg.get._2)
Out[53]:
In [54]:
normEqs == eqs.map(eq => TermData.isleNormalize(eq))
Out[54]:
In [55]:
normEqs -- eqs.map(eq => TermData.isleNormalize(eq))
Out[55]:
In [57]:
val badEq = eqs.find(eq => TermData.isleNormalize(eq) != TermData.isleNormalize(eq)).get
Out[57]:
In [58]:
val eq1 = TermData.isleNormalize(badEq)
Out[58]:
In [59]:
val eq2 = TermData.isleNormalize(badEq)
Out[59]:
In [60]:
eq1 == eq2
Out[60]:
In [61]:
eq1.rhs ==eq2.rhs
Out[61]:
In [62]:
eq1.rhs
Out[62]:
In [63]:
eq1.lhs == eq2.lhs
Out[63]:
In [64]:
eq1.lhs
Out[64]:
In [65]:
eq2.lhs
Out[65]:
In [67]:
import Expression._
val exp = badEq.lhs.asInstanceOf[FinalVal[Term]].variable
Out[67]:
In [68]:
import TermRandomVars._
val n1 = isleNormalizeVars(exp, Vector())
Out[68]:
In [69]:
val n2 = isleNormalizeVars(exp, Vector())
n1 == n2
Out[69]:
In [70]:
val i1 = n1.asInstanceOf[InIsle[Term, TermState, Term, Term]]
Out[70]:
In [71]:
val i2 = n2.asInstanceOf[InIsle[Term, TermState, Term, Term]]
Out[71]:
In [72]:
i1.boat == i2.boat
Out[72]:
In [73]:
i1.isleVar == i2.isleVar
Out[73]:
In [74]:
i1.isle == i2.isle
Out[74]:
In [75]:
i1.isle
Out[75]:
In [76]:
i2.isle
Out[76]:
In [77]:
i1.isle.initMap == i2.isle.initMap
Out[77]:
In [78]:
i1.isle.output == i2.isle.output
Out[78]:
In [79]:
i1.isle.islandOutput == i2.isle.islandOutput
Out[79]: