Goal

This is meant to try out the workflow, taking advantage of the filling in of future computations.

Before starting

In the console, we begin with

mill core.jvm.publishLocal

First steps

  • print out the git log HEAD for replication
  • import with ivy,
  • import provingground and the main packages,
  • bind to REPL to avoid verbose output.
In [12]:
import sys.process._
println("git log -1".!!)

commit a6ae52a12ec053bbe0202927e570658e8131e43c
Author: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
Date:   Fri Sep 13 15:18:38 2019 +0530

    removed lfs
Out[12]:
import sys.process._
In [30]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.0`
// import $ivy.`io.monix::monix:3.0.0`
Out[30]:
import $ivy.$                                                          
// import $ivy.`io.monix::monix:3.0.0`
In [31]:
import provingground._, interface._, learning._, translation._, HoTT._
Out[31]:
import provingground._, interface._, learning._, translation._, HoTT._

We will now explore without notes.

In [32]:
val tg = TermGenParams()
Out[32]:
tg: TermGenParams = 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
)
In [33]:
val terms = FiniteDistribution.unif[Term](Type, Unit, Zero, Star)
Out[33]:
terms: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(Universe(0), 0.25),
    Weighted(Unit, 0.25),
    Weighted(Zero, 0.25),
    Weighted(Star, 0.25)
  )
)
In [34]:
val typs = FiniteDistribution.unif[Typ[Term]](Type, Unit, Zero)
Out[34]:
typs: FiniteDistribution[Typ[Term]] = FiniteDistribution(
  Vector(
    Weighted(Universe(0), 0.3333333333333333),
    Weighted(Unit, 0.3333333333333333),
    Weighted(Zero, 0.3333333333333333)
  )
)
In [35]:
val ts = TermState(terms, typs)
val lp = LocalProver(ts)
Out[35]:
ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(Universe(0), 0.25),
      Weighted(Unit, 0.25),
      Weighted(Zero, 0.25),
      Weighted(Star, 0.25)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(Universe(0), 0.3333333333333333),
      Weighted(Unit, 0.3333333333333333),
      Weighted(Zero, 0.3333333333333333)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(Universe(0), 0.25),
        Weighted(Unit, 0.25),
        Weighted(Zero, 0.25),
        Weighted(Star, 0.25)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(Universe(0), 0.3333333333333333),
        Weighted(Unit, 0.3333333333333333),
        Weighted(Zero, 0.3333333333333333)
      )
    ),
    Vector(),
    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,
...

As everything important is supposed to be memoized, we can calculate anything and intermediate steps are remembered. So we calculate theorems.

In [19]:
val thmsT = lp.theoremsByStatement
Out[19]:
thmsT: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Map(
  FlatMap(
    Map(
      Async(<function2>, false, true, false),
      provingground.learning.LocalProver$$Lambda$2484/1295738439@28f0d7b9,
      0
    ),
    provingground.learning.LocalProver$$Lambda$2485/2069605659@5d0be5ed
  ),
  provingground.learning.LocalProverStep$$Lambda$2486/1615995408@28b2db83,
  0
)
In [22]:
val thmsF = thmsT.materialize.runToFuture

thmsF: monix.execution.CancelableFuture[scala.util.Try[FiniteDistribution[Typ[Term]]]] = Success(
  Failure(
    java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
  )
)
In [25]:
thmsF.value
Out[25]:
res24: Option[scala.util.Try[scala.util.Try[FiniteDistribution[Typ[Term]]]]] = Some(
  Success(
    Failure(
      java.util.concurrent.TimeoutException: Task timed-out after 12 minutes of inactivity
    )
  )
)

The main result of this experiment was a failure. Should investigate further. This could be because corrections for equations lead to a slowdown. Should try without generating equations.

In [36]:
val lp0 = LocalProver(ts, cutoff = 0.01)
Out[36]:
lp0: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(Universe(0), 0.25),
        Weighted(Unit, 0.25),
        Weighted(Zero, 0.25),
        Weighted(Star, 0.25)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(Universe(0), 0.3333333333333333),
        Weighted(Unit, 0.3333333333333333),
        Weighted(Zero, 0.3333333333333333)
      )
    ),
    Vector(),
    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,
...
In [37]:
val nsT = lp0.nextState
Out[37]:
nsT: monix.eval.Task[TermState] = FlatMap(
  Map(
    Async(<function2>, false, true, false),
    provingground.learning.LocalProver$$Lambda$2484/1295738439@28f0d7b9,
    0
  ),
  provingground.learning.LocalProver$$Lambda$2485/2069605659@52900737
)
In [38]:
val nsF = nsT.runToFuture

nsF: monix.execution.CancelableFuture[TermState] = [running future]
In [29]:
nsF.value
Out[29]:
res28: Option[scala.util.Try[TermState]] = None

Error with even a low cutoff, so clearly a bug. But the code ran fine in a REPL, so notebook issue.