notebook.community

Edit and run



In [1]:

    
import $cp.bin.`provingground-core-jvm.fat.jar`









    Out[1]:





import $cp.$

Fat jars work: Including a fat jar rather than local publishing has worked well.



In [2]:

    
import provingground._ , interface._, HoTT._, learning._









    Out[2]:





import provingground._ , interface._, HoTT._, learning._



In [3]:

    
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}



In [4]:

    
val terms = FiniteDistribution.unif[Term](Type, Unit, Zero, Star)









    Out[4]:





terms: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(𝒰 , 0.25),
    Weighted(Unit, 0.25),
    Weighted(Zero, 0.25),
    Weighted(Star, 0.25)
  )
)



In [5]:

    
val typs = FiniteDistribution.unif[Typ[Term]](Type, Unit, Zero)









    Out[5]:





typs: FiniteDistribution[Typ[Term]] = FiniteDistribution(
  Vector(
    Weighted(𝒰 , 0.3333333333333333),
    Weighted(Unit, 0.3333333333333333),
    Weighted(Zero, 0.3333333333333333)
  )
)



In [6]:

    
val ts = TermState(terms, typs)









    Out[6]:





ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(𝒰 , 0.25),
      Weighted(Unit, 0.25),
      Weighted(Zero, 0.25),
      Weighted(Star, 0.25)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(𝒰 , 0.3333333333333333),
      Weighted(Unit, 0.3333333333333333),
      Weighted(Zero, 0.3333333333333333)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)



In [7]:

    
val lp0 = LocalProver(ts, cutoff = 0.01)









    Out[7]:





lp0: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(𝒰 , 0.25),
        Weighted(Unit, 0.25),
        Weighted(Zero, 0.25),
        Weighted(Star, 0.25)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(𝒰 , 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 [8]:

    
val nsT = lp0.nextState









    Out[8]:





nsT: monix.eval.Task[TermState] = FlatMap(
  Map(
    Async(<function2>, false, true, true),
    provingground.learning.LocalProver$$Lambda$2573/891349477@334f7016,
    0
  ),
  provingground.learning.LocalProver$$Lambda$2574/712541575@3c2cac8a
)



In [9]:

    
import monix.execution.Scheduler.Implicits.global









    Out[9]:





import monix.execution.Scheduler.Implicits.global



In [10]:

    
val nsF = nsT.runToFuture









    





nsF: monix.execution.CancelableFuture[TermState] = Success(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(Zero, 0.25),
        Weighted(Unit, 0.25),
        Weighted(𝒰 , 0.25),
        Weighted(Star, 0.25)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(𝒰 , 0.3),
        Weighted((Zero → Unit), 0.016666666666666666),
        Weighted((Unit → Unit), 0.016666666666666666),
        Weighted(Zero, 0.3),
        Weighted((Zero → Zero), 0.016666666666666666),
        Weighted((Unit → Zero), 0.016666666666666666),
        Weighted((Zero → 𝒰 ), 0.016666666666666666),
        Weighted((Unit → 𝒰 ), 0.016666666666666666),
        Weighted(Unit, 0.3)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  )
)



In [11]:

    
nsF.value









    Out[11]:





res10: Option[scala.util.Try[TermState]] = None



In [12]:

    
val lp = LocalProver(ts).sharpen(10)
val thmsT = lp.theoremsByStatement 
val thmsF = thmsT.runToFuture









    





lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(𝒰 , 0.25),
        Weighted(Unit, 0.25),
        Weighted(Zero, 0.25),
        Weighted(Star, 0.25)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(𝒰 , 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,
...
thmsT: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Map(
  FlatMap(
    Map(
      Async(<function2>, false, true, true),
      provingground.learning.LocalProver$$Lambda$2573/891349477@334f7016,
      0
    ),
    provingground.learning.LocalProver$$Lambda$2574/712541575@167fc991
  ),
  provingground.learning.LocalProverStep$$Lambda$2791/1864253258@24401851,
  0
)
thmsF: monix.execution.CancelableFuture[FiniteDistribution[Typ[Term]]] = Success(
  FiniteDistribution(
    Vector(
      Weighted((Zero → (𝒰  → Unit)), 3.0497390746605195E-4),
      Weighted((Zero → (Zero → Unit)), 4.356770106657885E-4),
      Weighted((Zero → (Unit → Unit)), 4.356770106657885E-4),
      Weighted((𝒰  → (Zero → Unit)), 2.688606639440138E-4),
      Weighted((𝒰  → (𝒰  → Unit)), 1.8820246476080962E-4),
      Weighted((𝒰  → (Unit → Unit)), 2.688606639440138E-4),
      Weighted(∏(@a : 𝒰 ){ (@a → Unit) }, 3.4567799649944635E-4),
      Weighted((Unit → (Unit → Unit)), 4.3567701066578866E-4),
      Weighted((Unit → (Zero → Unit)), 4.3567701066578866E-4),
      Weighted((Unit → (𝒰  → Unit)), 3.04973907466052E-4),
      Weighted(𝒰 , 0.41378006453846056),
      Weighted(Unit×𝒰 , 0.006307547629305582),
      Weighted((𝒰  → Unit), 0.009476178164047663),
      Weighted((Zero → Unit), 0.015196691774522063),
      Weighted((𝒰 ×Zero → Unit), 1.6475595324836717E-4),
      Weighted(((Zero → Unit) → Unit), 3.873991333137281E-4),
      Weighted(((𝒰  → Unit) → Unit), 2.886934634346448E-4),
      Weighted((∑(@a : { @a } → Unit), 2.1182908274790062E-4),
      Weighted((Unit×Zero → Unit), 2.0476811332297058E-4),
      Weighted((Unit×Unit → Unit), 2.0476811332297058E-4),
      Weighted((Zero×𝒰  → Unit), 2.0476811332297058E-4),
      Weighted((Zero×Unit → Unit), 2.0476811332297058E-4),
      Weighted((𝒰 ×𝒰  → Unit), 1.6475595324836717E-4),
      Weighted(((Zero → Zero) → Unit), 3.873991333137281E-4),
      Weighted(((𝒰  → Zero) → Unit), 2.886934634346448E-4),
      Weighted((Unit → Unit), 0.01650481911361812),
      Weighted((Unit×𝒰  → Unit), 2.0476811332297058E-4),
      Weighted(((Unit → Unit) → Unit), 3.873991333137281E-4),
      Weighted(((Unit → Zero) → Unit), 3.873991333137281E-4),
      Weighted((Zero×Zero → Unit), 2.0476811332297058E-4),
      Weighted(((Zero → 𝒰 ) → Unit), 3.873991333137281E-4),
      Weighted(((𝒰  → 𝒰 ) → Unit), 2.474515400868384E-4),
      Weighted(((Unit → 𝒰 ) → Unit), 2.905493499852961E-4),
      Weighted((𝒰 ×Unit → Unit), 1.6475595324836717E-4),
      Weighted((∏(@a : 𝒰 ){ @a } → Unit), 3.7117731013025767E-4),
      Weighted(∑(@a : { @a }, 0.005079885089552229),
...



In [13]:

    
import scala.concurrent._, scala.util._
val fu = Future(())(ExecutionContext.global)
val fut = fu.flatMap(_ => thmsF)









    





import scala.concurrent._, scala.util._

fu: Future[Unit] = [running]
fut: Future[FiniteDistribution[Typ[Term]]] = Success(
  FiniteDistribution(
    Vector(
      Weighted((Zero → (𝒰  → Unit)), 3.0497390746605195E-4),
      Weighted((Zero → (Zero → Unit)), 4.356770106657885E-4),
      Weighted((Zero → (Unit → Unit)), 4.356770106657885E-4),
      Weighted((𝒰  → (Zero → Unit)), 2.688606639440138E-4),
      Weighted((𝒰  → (𝒰  → Unit)), 1.8820246476080962E-4),
      Weighted((𝒰  → (Unit → Unit)), 2.688606639440138E-4),
      Weighted(∏(@a : 𝒰 ){ (@a → Unit) }, 3.4567799649944635E-4),
      Weighted((Unit → (Unit → Unit)), 4.3567701066578866E-4),
      Weighted((Unit → (Zero → Unit)), 4.3567701066578866E-4),
      Weighted((Unit → (𝒰  → Unit)), 3.04973907466052E-4),
      Weighted(𝒰 , 0.41378006453846056),
      Weighted(Unit×𝒰 , 0.006307547629305582),
      Weighted((𝒰  → Unit), 0.009476178164047663),
      Weighted((Zero → Unit), 0.015196691774522063),
      Weighted((𝒰 ×Zero → Unit), 1.6475595324836717E-4),
      Weighted(((Zero → Unit) → Unit), 3.873991333137281E-4),
      Weighted(((𝒰  → Unit) → Unit), 2.886934634346448E-4),
      Weighted((∑(@a : { @a } → Unit), 2.1182908274790062E-4),
      Weighted((Unit×Zero → Unit), 2.0476811332297058E-4),
      Weighted((Unit×Unit → Unit), 2.0476811332297058E-4),
      Weighted((Zero×𝒰  → Unit), 2.0476811332297058E-4),
      Weighted((Zero×Unit → Unit), 2.0476811332297058E-4),
      Weighted((𝒰 ×𝒰  → Unit), 1.6475595324836717E-4),
      Weighted(((Zero → Zero) → Unit), 3.873991333137281E-4),
      Weighted(((𝒰  → Zero) → Unit), 2.886934634346448E-4),
      Weighted((Unit → Unit), 0.01650481911361812),
      Weighted((Unit×𝒰  → Unit), 2.0476811332297058E-4),
      Weighted(((Unit → Unit) → Unit), 3.873991333137281E-4),
      Weighted(((Unit → Zero) → Unit), 3.873991333137281E-4),
      Weighted((Zero×Zero → Unit), 2.0476811332297058E-4),
      Weighted(((Zero → 𝒰 ) → Unit), 3.873991333137281E-4),
      Weighted(((𝒰  → 𝒰 ) → Unit), 2.474515400868384E-4),
      Weighted(((Unit → 𝒰 ) → Unit), 2.905493499852961E-4),
      Weighted((𝒰 ×Unit → Unit), 1.6475595324836717E-4),
      Weighted((∏(@a : 𝒰 ){ @a } → Unit), 3.7117731013025767E-4),
      Weighted(∑(@a : { @a }, 0.005079885089552229),
...



In [14]:

    
thmsF.map(_.entropyVec)









    





res13: monix.execution.CancelableFuture[Vector[Weighted[Typ[Term]]]] = Success(
  Vector(
    Weighted(Unit, 1.1734179283216406),
    Weighted(𝒰 , 1.2730639554514531),
    Weighted((Unit → Unit), 5.920968862502742),
    Weighted((Zero → Zero), 5.924543546226858),
    Weighted((Zero → Unit), 6.040098897681761),
    Weighted((Zero → 𝒰 ), 6.093968394169324),
    Weighted((Unit → 𝒰 ), 6.102041157860943),
    Weighted((𝒰  → Unit), 6.721478961350752),
    Weighted((𝒰  → 𝒰 ), 6.721478961350752),
    Weighted(Unit×𝒰 , 7.308705089397329),
    Weighted(Unit×Unit, 7.308705089397329),
    Weighted(∑(@a : { @a }, 7.6209884220363335),
    Weighted(𝒰 ×𝒰 , 7.983558501421041),
    Weighted(𝒰 ×Unit, 7.983558501421041),
    Weighted(∏(@a : 𝒰 ){ (@a → @a) }, 11.135713525755705),
    Weighted((Zero → (Zero → Unit)), 11.16445339086257),
    Weighted((Zero → (Unit → Unit)), 11.16445339086257),
    Weighted((Unit → (Unit → Unit)), 11.16445339086257),
    Weighted((Unit → (Zero → Unit)), 11.16445339086257),
    Weighted((Zero → (Zero → 𝒰 )), 11.16445339086257),
    Weighted((Zero → (Unit → 𝒰 )), 11.16445339086257),
    Weighted((Unit → (Unit → 𝒰 )), 11.16445339086257),
    Weighted((Unit → (Zero → 𝒰 )), 11.16445339086257),
    Weighted((Zero → (Unit → Zero)), 11.16445339086257),
    Weighted((Zero → (Zero → Zero)), 11.16445339086257),
    Weighted((Unit → (Zero → Zero)), 11.16445339086257),
    Weighted(((Zero → Zero) → Unit), 11.333891653190589),
    Weighted(((Zero → Unit) → Unit), 11.333891653190589),
    Weighted(((Unit → Unit) → Unit), 11.333891653190589),
    Weighted(((Unit → Zero) → Unit), 11.333891653190589),
    Weighted(((Zero → 𝒰 ) → Unit), 11.333891653190589),
    Weighted(((Unit → Zero) → Zero), 11.333891653190589),
    Weighted(((Zero → Zero) → 𝒰 ), 11.333891653190589),
    Weighted(((Zero → Unit) → 𝒰 ), 11.333891653190589),
    Weighted(((Unit → Unit) → 𝒰 ), 11.333891653190589),
    Weighted(((Unit → Zero) → 𝒰 ), 11.333891653190589),
    Weighted(((Zero → 𝒰 ) → 𝒰 ), 11.333891653190589),
...



In [15]:

    
Future{Thread.sleep(1000); 5}(ExecutionContext.global)









    





res14: Future[Int] = Success(5)



In [16]:

    
Future{Thread.sleep(1000); Type ->: Type}(ExecutionContext.global)









    





res15: Future[FuncTyp[Typ[Term], Typ[Term]]] = Success((𝒰  → 𝒰 ))