Testing generation of inductive functions for non-parametrized, non-inductive definitions

We directly test the nodes for generating terms by recursive and inductive definitions on natural numbers, obtained by choosing codomain/target family and filling in recursion data.

In [1]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.0`
Out[1]:
import $ivy.$
In [2]:
import provingground._ , interface._, HoTT._
import provingground.{FiniteDistribution => FD}
import learning._
Out[2]:
import provingground._ , interface._, HoTT._

import provingground.{FiniteDistribution => FD}

import learning._

We define the inductive structure on the natural numbers.

In [3]:
val Nat = Type.sym
val zero = Nat.sym
val succ = (Nat ->: Nat).sym
val natIntros = Vector(zero, succ)
Out[3]:
Nat: Typ[Term] = SymbTyp(Name("Nat"), 0)
zero: Term = SymbObj(Name("zero"), SymbTyp(Name("Nat"), 0))
succ: Func[Term, Term] = SymbolicFunc(
  Name("succ"),
  SymbTyp(Name("Nat"), 0),
  SymbTyp(Name("Nat"), 0)
)
natIntros: Vector[Term] = Vector(
  SymbObj(Name("zero"), SymbTyp(Name("Nat"), 0)),
  SymbolicFunc(Name("succ"), SymbTyp(Name("Nat"), 0), SymbTyp(Name("Nat"), 0))
)
In [4]:
import induction._
val natStr = provingground.induction.ExstInducStrucs.get(Nat, natIntros)
Out[4]:
import induction._

natStr: ExstInducStrucs = ConsSeqExst(
  ConstructorSeqTL(
    Cons(
      Name("zero"),
      IdShape(),
      Cons(Name("succ"), FuncConsShape(IdIterShape(), IdShape()), Empty())
    ),
    SymbTyp(Name("Nat"), 0)
  ),
  Vector(
    SymbObj(Name("zero"), SymbTyp(Name("Nat"), 0)),
    SymbolicFunc(Name("succ"), SymbTyp(Name("Nat"), 0), SymbTyp(Name("Nat"), 0))
  )
)
In [5]:
val natDef = ExstInducDefn(Nat, natIntros, natStr)
Out[5]:
natDef: ExstInducDefn = ExstInducDefn(
  SymbTyp(Name("Nat"), 0),
  Vector(
    SymbObj(Name("zero"), SymbTyp(Name("Nat"), 0)),
    SymbolicFunc(Name("succ"), SymbTyp(Name("Nat"), 0), SymbTyp(Name("Nat"), 0))
  ),
  ConsSeqExst(
    ConstructorSeqTL(
      Cons(
        Name("zero"),
        IdShape(),
        Cons(Name("succ"), FuncConsShape(IdIterShape(), IdShape()), Empty())
      ),
      SymbTyp(Name("Nat"), 0)
    ),
    Vector(
      SymbObj(Name("zero"), SymbTyp(Name("Nat"), 0)),
      SymbolicFunc(
        Name("succ"),
        SymbTyp(Name("Nat"), 0),
        SymbTyp(Name("Nat"), 0)
      )
    )
  )
)

Next, we set up for generation

In [6]:
val ts = TermState(FD.unif(Nat, zero, succ), FD.unif(Nat, Type), inds = FD.unif(natDef))
val tg = TermGenParams()
Out[6]:
ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(SymbTyp(Name("Nat"), 0), 0.3333333333333333),
      Weighted(
        SymbObj(Name("zero"), SymbTyp(Name("Nat"), 0)),
        0.3333333333333333
      ),
      Weighted(
        SymbolicFunc(
          Name("succ"),
          SymbTyp(Name("Nat"), 0),
          SymbTyp(Name("Nat"), 0)
        ),
        0.3333333333333333
      )
    )
  ),
  FiniteDistribution(
    Vector(Weighted(SymbTyp(Name("Nat"), 0), 0.5), Weighted(Universe(0), 0.5))
  ),
  Vector(),
  FiniteDistribution(
    Vector(
      Weighted(
        ExstInducDefn(
          SymbTyp(Name("Nat"), 0),
          Vector(
            SymbObj(Name("zero"), SymbTyp(Name("Nat"), 0)),
            SymbolicFunc(
              Name("succ"),
              SymbTyp(Name("Nat"), 0),
              SymbTyp(Name("Nat"), 0)
            )
          ),
          ConsSeqExst(
            ConstructorSeqTL(
              Cons(
                Name("zero"),
...
tg: TermGenParams = TermGenParams(
  0.1,
  0.1,
  0.1,
  0.1,
  0.1,
  0.05,
  0.05,
  0.05,
  0.3,
  0.7,
  0.5
)
In [7]:
val mfd = tg.monixFD
Out[7]:
mfd: MonixFiniteDistribution[TermState, Term] = MonixFiniteDistribution(
  Cons(
    BaseCons(
      BasePi(
        provingground.learning.RandomVarFamily$$Lambda$3792/1544168874@63512837,
        FuncsWithDomain
      ),
      0.55,
      BaseCons(
        BasePi(
          provingground.learning.GeneratorNode$$Lambda$3795/657281012@4d10a987,
          FuncsWithDomain
        ),
        0.1,
        BaseCons(
          BasePi(
            provingground.learning.GeneratorNode$$Lambda$3795/657281012@3cac0434,
            FuncsWithDomain
          ),
          0.1,
          BaseCons(
            BasePi(
              provingground.learning.GeneratorNode$$Lambda$3795/657281012@7ca2c07c,
              FuncsWithDomain
            ),
            0.1,
            BaseCons(
              BasePi(
                provingground.learning.TermGeneratorNodes$$Lambda$3781/464466679@2890dfe5,
                FuncsWithDomain
              ),
              0.1,
              Target(FuncsWithDomain)
            )
          )
        )
...

A check that inductive types are picked up from the initial distribution.

In [8]:
import TermRandomVars._
val idT = mfd.varDist(ts)(InducDefns, 0.1)
Out[8]:
import TermRandomVars._

idT: monix.eval.Task[FiniteDistribution[ExstInducDefn]] = FlatMap(
  Async(<function2>, true, true, true),
  monix.eval.Task$$Lambda$3843/1159594218@5b483259
)
In [9]:
import monix.execution.Scheduler.Implicits.global 
repl.pprinter.bind(translation.FansiShow.fansiPrint)

val inducFD = idT.runSyncUnsafe()
Out[9]:
import monix.execution.Scheduler.Implicits.global 

inducFD: FiniteDistribution[ExstInducDefn] = FiniteDistribution(
  Vector(
    Weighted(
      ExstInducDefn(
        Nat,
        Vector(zero, succ),
        ConsSeqExst(
          ConstructorSeqTL(
            Cons(zero, IdShape(), Cons(succ, FuncConsShape(IdIterShape(), IdShape()), Empty())),
            Nat
          ),
          Vector(zero, succ)
        )
      ),
      1.0
    )
  )
)

Domain

We generate the domain from the inductive type. Nothing to do in the simple case.

In [10]:
val domT = mfd.varDist(ts)(domForInduc(natDef), 0.1)
Out[10]:
domT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Async(<function2>, true, true, true),
  monix.eval.Task$$Lambda$3843/1159594218@11dfcef1
)
In [11]:
val domFD = domT.runSyncUnsafe()
Out[11]:
domFD: FiniteDistribution[Term] = FiniteDistribution(Vector(Weighted(Nat, 1.0)))

Recursive definitions

We next define functions recursively

In [12]:
val ndT = mfd.nodeDist(ts)(tg.Gen.recFuncFoldedNode, 0.001)
Out[12]:
ndT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Map(
    FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$3843/1159594218@30448a1d),
    provingground.learning.MonixFiniteDistribution$$Lambda$3947/871931955@22e705f3,
    0
  ),
  provingground.learning.MonixFiniteDistribution$$Lambda$3948/634189918@1214adc6
)
In [13]:
val nfd = ndT.runSyncUnsafe()
Out[13]:
nfd: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(rec_{ Nat ; Nat }(succ(zero))((_ : Nat) ↦ (_ : Nat) ↦ zero), 0.007694285640620071),
    Weighted(
      rec_{ Nat ; Nat }(succ(succ(zero)))((_ : Nat) ↦ (_ : Nat) ↦ zero),
      0.006344070519242263
    ),
    Weighted(rec_{ Nat ; Nat }(succ(zero))((_ : Nat) ↦ succ), 0.09515789996358705),
    Weighted(rec_{ Nat ; Nat }(succ(succ(zero)))((_ : Nat) ↦ (@b : Nat) ↦ @b), 0.011652374423098036),
    Weighted(rec_{ Nat ; Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Nat) ↦ @a), 0.008156662096168625),
    Weighted(rec_{ Nat ; Nat }(zero)((@a : Nat) ↦ (_ : Nat) ↦ @a), 0.008270906578558813),
    Weighted(rec_{ Nat ; Nat }(zero)((_ : Nat) ↦ (@b : Nat) ↦ @b), 0.011815580826512592),
    Weighted(
      rec_{ Nat ; Nat }(succ(zero))((_ : Nat) ↦ (_ : Nat) ↦ succ(zero)),
      0.015388571281240142
    ),
    Weighted(rec_{ Nat ; Nat }(zero)((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)), 0.026519414743950483),
    Weighted(rec_{ Nat ; Nat }(succ(zero))((@a : Nat) ↦ (_ : Nat) ↦ @a), 0.009892652966511524),
    Weighted(rec_{ Nat ; Nat }(succ(zero))((_ : Nat) ↦ (@b : Nat) ↦ @b), 0.014132361380730747),
    Weighted(rec_{ Nat ; Nat }(succ(zero))((@a : Nat) ↦ (_ : Nat) ↦ succ(@a)), 0.019785305933023047),
    Weighted(rec_{ Nat ; Nat }(succ(zero))((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)), 0.028264722761461494),
    Weighted(rec_{ Nat ; Nat }(zero)((_ : Nat) ↦ succ), 0.053038829487900965),
    Weighted(rec_{ Nat ; 𝒰  }(Nat)((_ : Nat) ↦ (@a : 𝒰 ) ↦ @a), 0.27473350526106977),
    Weighted(rec_{ Nat ; Nat }(zero)((_ : Nat) ↦ (_ : Nat) ↦ zero), 0.0064329273388790765),
    Weighted(rec_{ Nat ; 𝒰  }(Nat)((_ : Nat) ↦ (_ : 𝒰 ) ↦ Nat), 0.14957713064213796),
    Weighted(rec_{ Nat ; Nat }(succ(succ(zero)))((_ : Nat) ↦ succ), 0.06395858850011588),
    Weighted(
      rec_{ Nat ; Nat }(succ(succ(zero)))((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)),
      0.037805481461606956
    )
  )
)
In [14]:
val nnT = mfd.varDist(ts)(termsWithTyp(Nat ->: Nat), 0.1)
Out[14]:
nnT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Async(<function2>, true, true, true),
  monix.eval.Task$$Lambda$3843/1159594218@6de1ac71
)
In [15]:
val nnD = nnT.runSyncUnsafe()
Out[15]:
nnD: FiniteDistribution[Term] = FiniteDistribution(Vector(Weighted(succ, 1.0)))
In [16]:
nfd.map(_.typ).flatten
Out[16]:
res15: FiniteDistribution[Typ[U] forSome { type U >: x$1 <: Term with Subs[U]; val x$1: Term }] = FiniteDistribution(
  Vector(Weighted((Nat β†’ 𝒰 ), 0.4243106359032077), Weighted((Nat β†’ Nat), 0.42431063590320767))
)

Inductive definitions

We make our first attempt at inductive definitions. We get some, but of only one type. We verify that this is because of the lack of richness in our initial state.

In [17]:
val nidT = mfd.nodeDist(ts)(tg.Gen.inducFuncFoldedNode, 0.00001)
Out[17]:
nidT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Map(
    FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$3843/1159594218@4fa408e6),
    provingground.learning.MonixFiniteDistribution$$Lambda$3947/871931955@22e705f3,
    0
  ),
  provingground.learning.MonixFiniteDistribution$$Lambda$3948/634189918@50744c00
)
In [18]:
val nifd = nidT.runSyncUnsafe()
Out[18]:
nifd: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((_ : Nat) ↦ (@b : Nat) ↦ succ(succ(succ(@b)))),
      0.0023818496077421827
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Nat) ↦ succ(succ(succ(@a)))),
      0.0016672947254195282
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(succ(succ(zero)))))((_ : Nat) ↦ (_ : Nat) ↦ succ(succ(zero))),
      0.0014088768310103873
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Nat) ↦ succ(@a)),
      0.003827612378330869
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)),
      0.005618820785853711
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((@a : Nat) ↦ (_ : Nat) ↦ succ(@a)),
      0.0030392922085904412
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)),
      0.004943166447340813
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((_ : Nat) ↦ (_ : Nat) ↦ succ(succ(zero))),
      0.0017671892134790885
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(succ(succ(zero)))))((_ : Nat) ↦ (@b : Nat) ↦ succ(succ(@b))),
      0.002693083607075716
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(succ(succ(zero)))))((@a : Nat) ↦ (_ : Nat) ↦ succ(succ(@a))),
      0.0018114130684419266
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((_ : Nat) ↦ (_ : Nat) ↦ succ(zero)),
...
In [19]:
nifd.map(_.typ).flatten
Out[19]:
res18: FiniteDistribution[Typ[U] forSome { type U >: x$1 <: Term with Subs[U]; val x$1: Term }] = FiniteDistribution(
  Vector(Weighted(∏(_ : Nat){ Nat }, 1.0))
)
In [20]:
termsWithTyp(typFamilyTarget(Nat).get)
val tfT = mfd.varDist(ts)(termsWithTyp(typFamilyTarget(Nat).get), 0.001)
Out[20]:
res19_0: RandomVar[Term] = AtCoord(TermsWithTyp, (Nat β†’ 𝒰 ) :: HNil)
tfT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Async(<function2>, true, true, true),
  monix.eval.Task$$Lambda$3843/1159594218@1236ae3b
)
In [21]:
val tfD = tfT.runSyncUnsafe()
Out[21]:
tfD: FiniteDistribution[Term] = FiniteDistribution(Vector(Weighted((_ : Nat) ↦ Nat, 1.0)))

More inductive definitions

We now enhance our generation state and see that we get inductive definitions including a simple proof.

In [22]:
val n = Nat.sym
val rel = (Nat ->: Type).sym
val allRel = (n ~>: rel(n)).sym
val ts1 = TermState(FD.unif(Nat, zero, succ, rel, allRel), FD.unif(Nat, Type), inds = FD.unif(natDef))
Out[22]:
n: Term = n
rel: Func[Term, Typ[Term]] = rel
allRel: FuncLike[Term, Term] = allRel
ts1: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(allRel, 0.2),
      Weighted(succ, 0.2),
      Weighted(Nat, 0.2),
      Weighted(zero, 0.2),
      Weighted(rel, 0.2)
    )
  ),
  FiniteDistribution(Vector(Weighted(Nat, 0.5), Weighted(𝒰 , 0.5))),
  Vector(),
  FiniteDistribution(
    Vector(
      Weighted(
        ExstInducDefn(
          Nat,
          Vector(zero, succ),
          ConsSeqExst(
            ConstructorSeqTL(
              Cons(zero, IdShape(), Cons(succ, FuncConsShape(IdIterShape(), IdShape()), Empty())),
              Nat
            ),
            Vector(zero, succ)
          )
        ),
        1.0
      )
    )
  ),
  FiniteDistribution(Vector()),
  Empty
)
In [23]:
val tfT1 = mfd.varDist(ts1)(termsWithTyp(typFamilyTarget(Nat).get), 0.001)
Out[23]:
tfT1: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Async(<function2>, true, true, true),
  monix.eval.Task$$Lambda$3843/1159594218@1bf1ac51
)
In [24]:
val tfD1 = tfT1.runSyncUnsafe()
Out[24]:
tfD1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted((_ : Nat) ↦ rel(succ(zero)), 0.013313167618019765),
    Weighted((_ : Nat) ↦ rel(zero), 0.08308884161040503),
    Weighted((@a : Nat) ↦ rel(succ(@a)), 0.10002632120794946),
    Weighted(rel, 0.5),
    Weighted((_ : Nat) ↦ Nat, 0.12552415182704352),
    Weighted((@a : Nat) ↦ rel(@a), 0.1780475177365822)
  )
)
In [25]:
val nidT1 = mfd.nodeDist(ts1)(tg.Gen.inducFuncFoldedNode, 0.000005)
val nifd1 = nidT1.runSyncUnsafe()
Out[25]:
nidT1: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Map(
    FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$3843/1159594218@702f975c),
    provingground.learning.MonixFiniteDistribution$$Lambda$3947/871931955@22e705f3,
    0
  ),
  provingground.learning.MonixFiniteDistribution$$Lambda$3948/634189918@db6196c
)
nifd1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Nat) ↦ succ(@a)),
      0.00103737820226554
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)),
      0.0016448077301823537
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)),
      0.0010637623519178623
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((@a : Nat) ↦ (_ : Nat) ↦ succ(@a)),
      7.446336463425035E-4
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((_ : Nat) ↦ (_ : Nat) ↦ succ(succ(zero))),
      1.2580564431652976E-4
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ rel(zero) }(allRel(zero))((_ : Nat) ↦ (_ : rel(zero)) ↦ allRel(zero)),
      0.009177109832656355
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((_ : Nat) ↦ (_ : Nat) ↦ succ(zero)),
      3.309061314077909E-4
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((@a : Nat) ↦ (_ : Nat) ↦ succ(succ(@a))),
      4.8514802748513203E-4
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((_ : Nat) ↦ (@b : Nat) ↦ succ(succ(@b))),
      6.930686106930457E-4
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((_ : Nat) ↦ (_ : Nat) ↦ zero),
      6.031788674726328E-4
    ),
    Weighted(
      induc_{ Nat ; ($beokh : Nat) ↦ rel($beokh) }(allRel(zero))((@a : Nat) ↦ (_ : rel(@a)) ↦ allRel(succ(@a))),
      0.8136105259883466
    ),
    Weighted(induc_{ Nat ; (_ : Nat) ↦ Nat }(zero)((_ : Nat) ↦ succ), 0.03707852791170968),
...
In [26]:
nifd1.map(_.typ).flatten
Out[26]:
res25: FiniteDistribution[Typ[U] forSome { type U >: x$1 <: Term with Subs[U]; val x$1: Term }] = FiniteDistribution(
  Vector(
    Weighted(∏(_ : Nat){ rel(zero) }, 0.03269327959759812),
    Weighted(∏(_ : Nat){ rel(succ(zero)) }, 0.009367215216334544),
    Weighted(∏($beokh : Nat){ rel($beokh) }, 0.8136105259883466),
    Weighted(∏(_ : Nat){ Nat }, 0.11250087767279501)
  )
)
In [27]:
val indF = natStr.inducOpt(Nat, n :-> rel(n)).get
Out[27]:
indF: Term = (InducDataSym(zero) : rel(zero)) ↦ (InducDataSym(succ) : ∏($dpexl : Nat){ (rel($dpexl) β†’ rel(succ($dpexl))) }) ↦ induc_{ Nat ; ($dpewb : Nat) ↦ rel($dpewb) }(InducDataSym(zero))(InducDataSym(succ))
In [28]:
indF.typ
Out[28]:
res27: Typ[U] = (rel(zero) β†’ (∏($dpexl : Nat){ (rel($dpexl) β†’ rel(succ($dpexl))) } β†’ ∏($dpewb : Nat){ rel($dpewb) }))
In [29]:
nifd1.filter(_.typ == n ~>: rel(n))
Out[29]:
res28: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      induc_{ Nat ; ($beokh : Nat) ↦ rel($beokh) }(allRel(zero))((@a : Nat) ↦ (_ : rel(@a)) ↦ allRel(succ(@a))),
      0.8136105259883466
    )
  )
)
In [30]:
val A = "A" :: Type
val List = "List" :: Type ->: Type
val nil = "nil" :: (A ~>: List(A))
val cons = "cons" :: A ~>: (A ->: List(A) ->: List(A))
Out[30]:
A: Typ[Term] = A
List: Func[Typ[Term], Typ[Term]] = List
nil: FuncLike[Typ[Term], Term] = nil
cons: FuncLike[Typ[Term], Func[Term, Func[Term, Term]]] = cons
In [31]:
val listAIntros = Vector(nil(A), cons(A))
val listAStr = ExstInducStrucs.get(List(A), listAIntros)
Out[31]:
listAIntros: Vector[Term] = Vector(nil(A), cons(A))
listAStr: ExstInducStrucs = ConsSeqExst(
  ConstructorSeqTL(
    Cons(
      (nil) (A),
      IdShape(),
      Cons((cons) (A), CnstFuncConsShape(A, FuncConsShape(IdIterShape(), IdShape())), Empty())
    ),
    List(A)
  ),
  Vector(nil(A), cons(A))
)
In [32]:
val listStr = ExstInducStrucs.LambdaInduc(A, listAStr)
Out[32]:
listStr: ExstInducStrucs.LambdaInduc = LambdaInduc(
  A,
  ConsSeqExst(
    ConstructorSeqTL(
      Cons(
        (nil) (A),
        IdShape(),
        Cons((cons) (A), CnstFuncConsShape(A, FuncConsShape(IdIterShape(), IdShape())), Empty())
      ),
      List(A)
    ),
    Vector(nil(A), cons(A))
  )
)
In [33]:
val listDef = ExstInducDefn(List, Vector(nil, cons) ,listStr)
Out[33]:
listDef: ExstInducDefn = ExstInducDefn(
  List,
  Vector(nil, cons),
  LambdaInduc(
    A,
    ConsSeqExst(
      ConstructorSeqTL(
        Cons(
          (nil) (A),
          IdShape(),
          Cons((cons) (A), CnstFuncConsShape(A, FuncConsShape(IdIterShape(), IdShape())), Empty())
        ),
        List(A)
      ),
      Vector(nil(A), cons(A))
    )
  )
)
In [34]:
val tsL = TermState(FD.unif(Nat, zero, succ, List, nil, cons), FD.unif(Nat, Type), inds = FD.unif(natDef, listDef))
Out[34]:
tsL: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(nil, 0.16666666666666666),
      Weighted(zero, 0.16666666666666666),
      Weighted(cons, 0.16666666666666666),
      Weighted(Nat, 0.16666666666666666),
      Weighted(List, 0.16666666666666666),
      Weighted(succ, 0.16666666666666666)
    )
  ),
  FiniteDistribution(Vector(Weighted(Nat, 0.5), Weighted(𝒰 , 0.5))),
  Vector(),
  FiniteDistribution(
    Vector(
      Weighted(
        ExstInducDefn(
          Nat,
          Vector(zero, succ),
          ConsSeqExst(
            ConstructorSeqTL(
              Cons(zero, IdShape(), Cons(succ, FuncConsShape(IdIterShape(), IdShape()), Empty())),
              Nat
            ),
            Vector(zero, succ)
          )
        ),
        0.5
      ),
      Weighted(
        ExstInducDefn(
          List,
          Vector(nil, cons),
          LambdaInduc(
            A,
            ConsSeqExst(
              ConstructorSeqTL(
                Cons(
                  (nil) (A),
                  IdShape(),
                  Cons(
                    (cons) (A),
                    CnstFuncConsShape(A, FuncConsShape(IdIterShape(), IdShape())),
                    Empty()
                  )
                ),
                List(A)
              ),
              Vector(nil(A), cons(A))
...
In [ ]:
In [35]:
val domLT = mfd.varDist(ts)(domForInduc(listDef), 0.00001)
Out[35]:
domLT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Async(<function2>, true, true, true),
  monix.eval.Task$$Lambda$3843/1159594218@46dde1e2
)
In [36]:
val domLD = domLT.runSyncUnsafe()
Out[36]:
domLD: FiniteDistribution[Term] = FiniteDistribution(
  Vector(Weighted(List((Nat β†’ Nat)), 9.567012510526363E-4), Weighted(List(Nat), 0.9990432987489474))
)
In [37]:
val ndLT = mfd.nodeDist(tsL)(tg.Gen.recFuncFoldedNode, 0.0001)
Out[37]:
ndLT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Map(
    FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$3843/1159594218@439a4e38),
    provingground.learning.MonixFiniteDistribution$$Lambda$3947/871931955@22e705f3,
    0
  ),
  provingground.learning.MonixFiniteDistribution$$Lambda$3948/634189918@566701dd
)
In [38]:
val ndLD = ndLT.runSyncUnsafe()
Out[38]:
ndLD: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      rec_{ List(List(List(Nat))) ; 𝒰  }(List(Nat))((_ : List(List(Nat))) ↦ (_ : List(List(List(Nat)))) ↦ (@a : 𝒰 ) ↦ @a),
      0.011876025054261429
    ),
    Weighted(
      rec_{ List(Nat) ; 𝒰  }(List(Nat))((_ : Nat) ↦ (_ : List(Nat)) ↦ List),
      0.024838099482446346
    ),
    Weighted(
      rec_{ List(List(Nat)) ; Nat }(zero)((_ : List(Nat)) ↦ (_ : List(List(Nat))) ↦ (@a : Nat) ↦ @a),
      0.005371146116496761
    ),
    Weighted(
      rec_{ List(List(List(Nat))) ; 𝒰  }(Nat)((_ : List(List(Nat))) ↦ (_ : List(List(List(Nat)))) ↦ List),
      0.004713022535422637
    ),
    Weighted(
      rec_{ List(List(List(Nat))) ; Nat }(zero)((_ : List(List(Nat))) ↦ (_ : List(List(List(Nat)))) ↦ succ),
      0.004713022535422637
    ),
    Weighted(rec_{ List(Nat) ; 𝒰  }(Nat)((_ : Nat) ↦ (_ : List(Nat)) ↦ List), 0.008279366494148782),
    Weighted(
      rec_{ List(Nat) ; Nat }(succ(zero))((@a : Nat) ↦ (_ : List(Nat)) ↦ (_ : Nat) ↦ succ(@a)),
      0.002517136577673004
    ),
    Weighted(
      rec_{ List(Nat) ; Nat }(succ(zero))((_ : Nat) ↦ (_ : List(Nat)) ↦ (@b : Nat) ↦ succ(@b)),
      0.013770049872190753
    ),
    Weighted(
      rec_{ List(List(List(Nat))) ; 𝒰  }(Nat)((_ : List(List(Nat))) ↦ (_ : List(List(List(Nat)))) ↦ (_ : 𝒰 ) ↦ Nat),
      7.543475173354943E-4
    ),
    Weighted(
      rec_{ List(Nat) ; Nat }(succ(zero))((_ : Nat) ↦ (_ : List(Nat)) ↦ succ),
      0.02492022289823205
    ),
    Weighted(
      rec_{ List(List(Nat)) ; Nat }(succ(zero))((_ : List(Nat)) ↦ (_ : List(List(Nat))) ↦ succ),
      0.019183943546087597
    ),
...
In [39]:
ndLD.map(_.typ).flatten
Out[39]:
res38: FiniteDistribution[Typ[U] forSome { type U >: x$1 <: Term with Subs[U]; val x$1: Term }] = FiniteDistribution(
  Vector(
    Weighted((Nat β†’ (List(Nat) β†’ Nat)), 0.0038234979779664816),
    Weighted((Nat β†’ (𝒰  β†’ Nat)), 0.003355421330769112),
    Weighted((List(Nat) β†’ List(Nat)), 0.022873118360534392),
    Weighted((List(List(Nat)) β†’ List(Nat)), 0.02209525361376903),
    Weighted((List(List(List(Nat))) β†’ List(Nat)), 0.0167018088689114),
    Weighted((Nat β†’ List(Nat)), 0.05340219573467698),
    Weighted((List(List(Nat)) β†’ Nat), 0.05115718278956693),
    Weighted((List(List(List(Nat))) β†’ Nat), 0.0377041802833811),
    Weighted((List(Nat) β†’ Nat), 0.0664539277286188),
    Weighted((Nat β†’ Nat), 0.15430368002512065),
    Weighted((List(List(List(Nat))) β†’ 𝒰 ), 0.03770418028338109),
    Weighted((List(Nat) β†’ 𝒰 ), 0.06623493195319026),
    Weighted((List(List(Nat)) β†’ 𝒰 ), 0.050963433793644444),
    Weighted((Nat β†’ 𝒰 ), 0.1538045651997658),
    Weighted((Nat β†’ (List(Nat) β†’ List(Nat))), 0.0031862483149720684),
    Weighted((Nat β†’ (Nat β†’ 𝒰 )), 0.004553786091758079),
    Weighted((Nat β†’ (List(Nat) β†’ 𝒰 )), 0.0038234979779664816),
    Weighted((Nat β†’ ∏(@a : 𝒰 ){ List(@a) }), 0.0028760754263735255)
  )
)
In [40]:
ndLD.support.size
Out[40]:
res39: Int = 93
In [41]:
val fns = ndLD.support.groupBy(_.typ)
Out[41]:
fns: Map[Typ[U] forSome { type U >: x$1 <: Term with Subs[U]; val x$1: Term }, Set[Term]] = Map(
  (Nat β†’ (List(Nat) β†’ Nat)) -> Set(
    rec_{ Nat ; (List(Nat) β†’ Nat) }((_ : List(Nat)) ↦ zero)((_ : Nat) ↦ (@a : (List(Nat) β†’ Nat)) ↦ @a)
  ),
  (Nat β†’ (𝒰  β†’ Nat)) -> Set(
    rec_{ Nat ; (𝒰  β†’ Nat) }((_ : 𝒰 ) ↦ zero)((_ : Nat) ↦ (@a : (𝒰  β†’ Nat)) ↦ @a)
  ),
  (List(List(List(Nat))) β†’ List(Nat)) -> Set(
    rec_{ List(List(List(Nat))) ; List(Nat) }(nil(Nat))((_ : List(List(Nat))) ↦ (_ : List(List(List(Nat)))) ↦ (@a : List(Nat)) ↦ @a)
  ),
  (List(List(Nat)) β†’ List(Nat)) -> Set(
    rec_{ List(List(Nat)) ; List(Nat) }(nil(Nat))((@a : List(Nat)) ↦ (_ : List(List(Nat))) ↦ (_ : List(Nat)) ↦ @a),
    rec_{ List(List(Nat)) ; List(Nat) }(nil(Nat))((_ : List(Nat)) ↦ (_ : List(List(Nat))) ↦ (@b : List(Nat)) ↦ @b)
  ),
  (Nat β†’ List(Nat)) -> Set(
    rec_{ Nat ; List(Nat) }(nil(Nat))((@a : Nat) ↦ cons(Nat)(@a)),
    rec_{ Nat ; List(Nat) }(nil(Nat))(cons(Nat)),
    rec_{ Nat ; List(Nat) }(nil(Nat))((_ : Nat) ↦ cons(Nat)(zero)),
    rec_{ Nat ; List(Nat) }(nil(Nat))((_ : Nat) ↦ (@a : List(Nat)) ↦ @a),
    rec_{ Nat ; List(Nat) }(nil(Nat))((_ : Nat) ↦ (_ : List(Nat)) ↦ nil(Nat))
  ),
  (List(Nat) β†’ List(Nat)) -> Set(
    rec_{ List(Nat) ; List(Nat) }(nil(Nat))((_ : Nat) ↦ (@a : List(Nat)) ↦ (_ : List(Nat)) ↦ @a),
    rec_{ List(Nat) ; List(Nat) }(nil(Nat))((_ : Nat) ↦ (_ : List(Nat)) ↦ (@b : List(Nat)) ↦ @b)
  ),
  (Nat β†’ Nat) -> Set(
    rec_{ Nat ; Nat }(succ(zero))((_ : Nat) ↦ (_ : Nat) ↦ zero),
    rec_{ Nat ; Nat }(succ(succ(zero)))((_ : Nat) ↦ (_ : Nat) ↦ zero),
    rec_{ Nat ; Nat }(succ(zero))((_ : Nat) ↦ succ),
    rec_{ Nat ; Nat }(succ(succ(zero)))((_ : Nat) ↦ (@b : Nat) ↦ @b),
    rec_{ Nat ; Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Nat) ↦ @a),
    rec_{ Nat ; Nat }(zero)((@a : Nat) ↦ (_ : Nat) ↦ @a),
    rec_{ Nat ; Nat }(zero)((_ : Nat) ↦ (@b : Nat) ↦ @b),
    rec_{ Nat ; Nat }(succ(zero))((_ : Nat) ↦ (_ : Nat) ↦ succ(zero)),
    rec_{ Nat ; Nat }(zero)((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)),
    rec_{ Nat ; Nat }(zero)((@a : Nat) ↦ (_ : Nat) ↦ succ(@a)),
    rec_{ Nat ; Nat }(succ(zero))((@a : Nat) ↦ (_ : Nat) ↦ @a),
    rec_{ Nat ; Nat }(succ(zero))((_ : Nat) ↦ (@b : Nat) ↦ @b),
    rec_{ Nat ; Nat }(succ(zero))((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)),
    rec_{ Nat ; Nat }(succ(zero))((@a : Nat) ↦ (_ : Nat) ↦ succ(@a)),
    rec_{ Nat ; Nat }(zero)((_ : Nat) ↦ succ),
    rec_{ Nat ; Nat }(zero)((_ : Nat) ↦ (_ : Nat) ↦ zero),
    rec_{ Nat ; Nat }(zero)((_ : Nat) ↦ (_ : Nat) ↦ succ(zero)),
    rec_{ Nat ; Nat }(succ(succ(zero)))((_ : Nat) ↦ succ),
    rec_{ Nat ; Nat }(succ(succ(zero)))((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)),
...
In [42]:
val lToL = fns(List(Nat) ->: List(Nat))
Out[42]:
lToL: Set[Term] = Set(
  rec_{ List(Nat) ; List(Nat) }(nil(Nat))((_ : Nat) ↦ (@a : List(Nat)) ↦ (_ : List(Nat)) ↦ @a),
  rec_{ List(Nat) ; List(Nat) }(nil(Nat))((_ : Nat) ↦ (_ : List(Nat)) ↦ (@b : List(Nat)) ↦ @b)
)
In [43]:
nil(Nat).typ
cons(Nat).typ
Out[43]:
res42_0: Typ[U] = List(Nat)
res42_1: Typ[Func[Term, Func[Term, Term]]] = (Nat β†’ (List(Nat) β†’ List(Nat)))
In [44]:
val l0 = cons(Nat)(zero)(nil(Nat))
Out[44]:
l0: Term = cons(Nat)(zero)(nil(Nat))
In [45]:
val l1 = cons(Nat)(succ(zero))(l0)
Out[45]:
l1: Term = cons(Nat)(succ(zero))(cons(Nat)(zero)(nil(Nat)))
In [46]:
import Fold._
lToL.map(fn => fn(l1))
Out[46]:
import Fold._

res45_1: Set[Term] = Set(nil(Nat), cons(Nat)(zero)(nil(Nat)))
In [47]:
val Vec = "Vec" :: Type ->: Nat ->: Type
val vnil = "vnil" :: (A ~>: Vec(A)(zero))
val vcons = "vcons" :: A ~>: (n ~>: (A ->: Vec(A)(n) ->: Vec(A)(succ(n))))
Out[47]:
Vec: Func[Typ[Term], Func[Term, Typ[Term]]] = Vec
vnil: FuncLike[Typ[Term], Term] = vnil
vcons: FuncLike[Typ[Term], FuncLike[Term, Func[Term, Func[Term, Term]]]] = vcons
In [48]:
val vecAIntros = Vector(vnil(A), vcons(A))
val vecAStr = ExstInducStrucs.getIndexed(Vec(A), vecAIntros)
Out[48]:
vecAIntros: Vector[Term] = Vector(vnil(A), vcons(A))
vecAStr: ExstInducStrucs = IndConsSeqExst(
  Cons(
    (vnil) (A),
    IndexedIdShape(FuncTypFamily(Nat, IdTypFamily()), zero :: HNil),
    Cons(
      (vcons) (A),
      IndexedCnstDepFuncConsShape(
        Nat,
        provingground.induction.TypFamilyExst$IndexedConstructorShapeExst$$Lambda$4481/467783333@1ab80398
      ),
      Empty(Vec(A), FuncTypFamily(Nat, IdTypFamily()))
    )
  ),
  Vector(vnil(A), vcons(A))
)
In [49]:
val vecStr = ExstInducStrucs.LambdaInduc(A, vecAStr)
Out[49]:
vecStr: ExstInducStrucs.LambdaInduc = LambdaInduc(
  A,
  IndConsSeqExst(
    Cons(
      (vnil) (A),
      IndexedIdShape(FuncTypFamily(Nat, IdTypFamily()), zero :: HNil),
      Cons(
        (vcons) (A),
        IndexedCnstDepFuncConsShape(
          Nat,
          provingground.induction.TypFamilyExst$IndexedConstructorShapeExst$$Lambda$4481/467783333@1ab80398
        ),
        Empty(Vec(A), FuncTypFamily(Nat, IdTypFamily()))
      )
    ),
    Vector(vnil(A), vcons(A))
  )
)
In [50]:
val vecDef = ExstInducDefn(Vec, Vector(vnil, vcons) ,vecStr)
val tsV = TermState(FD.unif(Nat, zero, succ, Vec, vnil, vcons), FD.unif(Nat, Type), inds = FD.unif(vecDef))
Out[50]:
vecDef: ExstInducDefn = ExstInducDefn(
  Vec,
  Vector(vnil, vcons),
  LambdaInduc(
    A,
    IndConsSeqExst(
      Cons(
        (vnil) (A),
        IndexedIdShape(FuncTypFamily(Nat, IdTypFamily()), zero :: HNil),
        Cons(
          (vcons) (A),
          IndexedCnstDepFuncConsShape(
            Nat,
            provingground.induction.TypFamilyExst$IndexedConstructorShapeExst$$Lambda$4481/467783333@1ab80398
          ),
          Empty(Vec(A), FuncTypFamily(Nat, IdTypFamily()))
        )
      ),
      Vector(vnil(A), vcons(A))
    )
  )
)
tsV: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(zero, 0.16666666666666666),
      Weighted(Nat, 0.16666666666666666),
      Weighted(Vec, 0.16666666666666666),
      Weighted(succ, 0.16666666666666666),
      Weighted(vnil, 0.16666666666666666),
      Weighted(vcons, 0.16666666666666666)
    )
  ),
  FiniteDistribution(Vector(Weighted(Nat, 0.5), Weighted(𝒰 , 0.5))),
  Vector(),
  FiniteDistribution(
    Vector(
      Weighted(
        ExstInducDefn(
          Vec,
          Vector(vnil, vcons),
          LambdaInduc(
            A,
            IndConsSeqExst(
              Cons(
                (vnil) (A),
                IndexedIdShape(FuncTypFamily(Nat, IdTypFamily()), zero :: HNil),
                Cons(
                  (vcons) (A),
                  IndexedCnstDepFuncConsShape(
                    Nat,
                    provingground.induction.TypFamilyExst$IndexedConstructorShapeExst$$Lambda$4481/467783333@1ab80398
                  ),
                  Empty(Vec(A), FuncTypFamily(Nat, IdTypFamily()))
                )
              ),
              Vector(vnil(A), vcons(A))
            )
          )
        ),
        1.0
      )
    )
  ),
  FiniteDistribution(Vector()),
  Empty
)
In [51]:
val domVT = mfd.varDist(ts)(domForInduc(vecDef), 0.00001)
Out[51]:
domVT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Async(<function2>, true, true, true),
  monix.eval.Task$$Lambda$3843/1159594218@672a8bdf
)
In [52]:
val domVD = domVT.runSyncUnsafe()
Out[52]:
domVD: FiniteDistribution[Term] = FiniteDistribution(
  Vector(Weighted(Vec(Nat), 0.9990432987489474), Weighted(Vec((Nat β†’ Nat)), 9.567012510526363E-4))
)
In [53]:
val ndVT = mfd.nodeDist(tsV)(tg.Gen.recFuncFoldedNode, 0.0001)
Out[53]:
ndVT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Map(
    FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$3843/1159594218@6ae4d806),
    provingground.learning.MonixFiniteDistribution$$Lambda$3947/871931955@22e705f3,
    0
  ),
  provingground.learning.MonixFiniteDistribution$$Lambda$3948/634189918@59e9a76f
)
In [54]:
val ndVD = ndVT.runSyncUnsafe()
Out[54]:
ndVD: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      ($frsjt : Nat) ↦ rec_{ Vec(Vec(Nat)(zero)) ; 𝒰  }(Nat)((@a : Nat) ↦ (_ : Vec(Nat)(zero)) ↦ (_ : Vec(Vec(Nat)(zero))(@a)) ↦ (@a : 𝒰 ) ↦ @a),
      0.05428832685110763
    ),
    Weighted(
      ($gfezi : Nat) ↦ rec_{ Vec(Vec(Nat)(succ(zero))) ; Vec(Nat)(zero) }(vnil(Nat))((@a : Nat) ↦ (_ : Vec(Nat)(succ(zero))) ↦ (_ : Vec(Vec(Nat)(succ(zero)))(@a)) ↦ (@a : Vec(Nat)(zero)) ↦ @a),
      0.038431121021796
    ),
    Weighted(
      ($gkhlv : Nat) ↦ rec_{ Vec(Vec(Nat)(succ(zero))) ; Nat }(zero)((@a : Nat) ↦ (_ : Vec(Nat)(succ(zero))) ↦ (_ : Vec(Vec(Nat)(succ(zero)))(@a)) ↦ succ),
      0.008099343924690992
    ),
    Weighted(
      ($fovqr : Nat) ↦ rec_{ Vec(Nat) ; 𝒰  }(Vec(Nat)(zero))((@a : Nat) ↦ (_ : Nat) ↦ (_ : Vec(Nat)(@a)) ↦ (_ : 𝒰 ) ↦ Nat),
      0.007617194402665406
    ),
    Weighted(
      ($fyucp : Nat) ↦ rec_{ Vec(Nat) ; Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Nat) ↦ (_ : Vec(Nat)(@a)) ↦ (_ : Nat) ↦ @a),
      0.001350080875687455
    ),
    Weighted(
      ($fyucp : Nat) ↦ rec_{ Vec(Nat) ; Nat }(succ(succ(zero)))((@a : Nat) ↦ (@b : Nat) ↦ (_ : Vec(Nat)(@a)) ↦ (_ : Nat) ↦ @b),
      0.001928686965267793
    ),
    Weighted(
      ($fyucp : Nat) ↦ rec_{ Vec(Nat) ; Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Nat) ↦ (_ : Vec(Nat)(@a)) ↦ (@c : Nat) ↦ @c),
      0.003936095847485292
    ),
    Weighted(
      ($fovqr : Nat) ↦ rec_{ Vec(Nat) ; 𝒰  }(Nat)((@a : Nat) ↦ (_ : Nat) ↦ (_ : Vec(Nat)(@a)) ↦ (_ : 𝒰 ) ↦ Nat),
      0.008719560013732548
    ),
    Weighted(
      ($fyucp : Nat) ↦ rec_{ Vec(Nat) ; Nat }(succ(zero))((@a : Nat) ↦ (_ : Nat) ↦ (_ : Vec(Nat)(@a)) ↦ (@c : Nat) ↦ succ(@c)),
      0.011407511741870428
    ),
    Weighted(
      ($fyucp : Nat) ↦ rec_{ Vec(Nat) ; Nat }(succ(zero))((@a : Nat) ↦ (@b : Nat) ↦ (_ : Vec(Nat)(@a...
In [55]:
ndVD.map(_.typ)
Out[55]:
res54: FiniteDistribution[Typ[U] forSome { type U >: x$1 <: Term with Subs[U]; val x$1: Term }] = FiniteDistribution(
  Vector(
    Weighted(∏($frsjt : Nat){ (Vec(Vec(Nat)(zero))($frsjt) β†’ 𝒰 ) }, 0.05428832685110763),
    Weighted(
      ∏($gfezi : Nat){ (Vec(Vec(Nat)(succ(zero)))($gfezi) β†’ Vec(Nat)(zero)) },
      0.038431121021796
    ),
    Weighted(∏($gkhlv : Nat){ (Vec(Vec(Nat)(succ(zero)))($gkhlv) β†’ Nat) }, 0.008099343924690992),
    Weighted(∏($fovqr : Nat){ (Vec(Nat)($fovqr) β†’ 𝒰 ) }, 0.007617194402665406),
    Weighted(∏($fyucp : Nat){ (Vec(Nat)($fyucp) β†’ Nat) }, 0.001350080875687455),
    Weighted(∏($fyucp : Nat){ (Vec(Nat)($fyucp) β†’ Nat) }, 0.001928686965267793),
    Weighted(∏($fyucp : Nat){ (Vec(Nat)($fyucp) β†’ Nat) }, 0.003936095847485292),
    Weighted(∏($fovqr : Nat){ (Vec(Nat)($fovqr) β†’ 𝒰 ) }, 0.008719560013732548),
    Weighted(∏($fyucp : Nat){ (Vec(Nat)($fyucp) β†’ Nat) }, 0.011407511741870428),
    Weighted(∏($fyucp : Nat){ (Vec(Nat)($fyucp) β†’ Nat) }, 0.00558968075351651),
    Weighted(∏($flyaa : Nat){ (Vec(Vec(Nat)(succ(zero)))($flyaa) β†’ 𝒰 ) }, 0.007191896155590722),
    Weighted(∏($fyucp : Nat){ (Vec(Nat)($fyucp) β†’ Nat) }, 0.03942879683447049),
    Weighted(∏($gpncs : Nat){ (Vec(Vec(Nat)(zero))($gpncs) β†’ Nat) }, 0.013566273517513399),
    Weighted(∏($gpncs : Nat){ (Vec(Vec(Nat)(zero))($gpncs) β†’ Nat) }, 0.004653231816507095),
    Weighted(∏($fxahs : Nat){ (Vec(Nat)($fxahs) β†’ Vec(Nat)(zero)) }, 0.06157214352649074),
    Weighted(∏($fyucp : Nat){ (Vec(Nat)($fyucp) β†’ Nat) }, 0.0015216353162350493),
    Weighted(∏($gpncs : Nat){ (Vec(Vec(Nat)(zero))($gpncs) β†’ Nat) }, 0.021056044202520427),
    Weighted(∏($gpncs : Nat){ (Vec(Vec(Nat)(zero))($gpncs) β†’ Nat) }, 0.007222223161464506),
    Weighted(∏($gpncs : Nat){ (Vec(Vec(Nat)(zero))($gpncs) β†’ Nat) }, 0.031086909704554466),
    Weighted(∏($frsjt : Nat){ (Vec(Vec(Nat)(zero))($frsjt) β†’ 𝒰 ) }, 0.004978503473835429),
    Weighted(∏($fyucp : Nat){ (Vec(Nat)($fyucp) β†’ Nat) }, 0.02729243486208059),
    Weighted(∏($frsjt : Nat){ (Vec(Vec(Nat)(zero))($frsjt) β†’ 𝒰 ) }, 0.007241459598306077),
    Weighted(∏($gkgrq : Nat){ (Vec(Vec(Nat)(zero))($gkgrq) β†’ Vec(Nat)(zero)) }, 0.01571793594795055),
    Weighted(
      ∏($gkgrq : Nat){ (Vec(Vec(Nat)(zero))($gkgrq) β†’ Vec(Nat)(zero)) },
      0.032077420301939906
    ),
    Weighted(∏($gpncs : Nat){ (Vec(Vec(Nat)(zero))($gpncs) β†’ Nat) }, 0.0028086423405695293),
    Weighted(∏($flyaa : Nat){ (Vec(Vec(Nat)(succ(zero)))($flyaa) β†’ 𝒰 ) }, 0.05391675585199211),
    Weighted(∏($frsjt : Nat){ (Vec(Vec(Nat)(zero))($frsjt) β†’ 𝒰 ) }, 0.0373232247101365),
    Weighted(∏($fovqr : Nat){ (Vec(Nat)($fovqr) β†’ 𝒰 ) }, 0.06536946282681629),
    Weighted(∏($gpncs : Nat){ (Vec(Vec(Nat)(zero))($gpncs) β†’ Nat) }, 0.0018095901508638698),
    Weighted(∏($fyucp : Nat){ (Vec(Nat)($fyucp) β†’ Nat) }, 0.007739895140096773),
    Weighted(∏($gkhlv : Nat){ (Vec(Vec(Nat)(succ(zero)))($gkhlv) β†’ Nat) }, 0.002096110640642589),
    Weighted(∏($fyucp : Nat){ (Vec(Nat)($fyucp) β†’ Nat) }, 0.0018513670321756036),
    Weighted(∏($gpncs : Nat){ (Vec(Vec(Nat)(zero))($gpncs) β†’ Nat) }, 0.020029095484884366),
    Weighted(∏($fovqr : Nat){ (Vec(Nat)($fovqr) β†’ 𝒰 ) }, 0.057105164201573244),
    Weighted(∏($gkhlv : Nat){ (Vec(Vec(Nat)(succ(zero)))($gkhlv) β†’ Nat) }, 0.0054859149819167586),
    Weighted(∏($gkhlv : Nat){ (Vec(Vec(Nat)(succ(zero)))($gkhlv) β†’ Nat) }, 0.0018816688387974481),
    Weighted(∏($gkhlv : Nat){ (Vec(Vec(Nat)(succ(zero)))($gkhlv) β†’ Nat) }, 0.023200391618107795),
    Weighted(∏($gkhlv : Nat){ (Vec(Vec(Nat)(succ(zero)))($gkhlv) β†’ Nat) }, 0.015714282187241406),
    Weighted(∏($gkhlv : Nat){ (Vec(Vec(Nat)(succ(zero)))($gkhlv) β†’ Nat) }, 0.005389998790223801),
    Weighted(∏($fyucp : Nat){ (Vec(Nat)($fyucp) β†’ Nat) }, 0.003912776527461557),
...
In [56]:
val vfn = vecStr.recOpt(Vec(Nat), A).get
Out[56]:
vfn: Term = (RecDataSym((vnil) (Nat)) : A) ↦ (RecDataSym((vcons) (Nat)) : ∏($iegjx : Nat){ (Nat β†’ (Vec(Nat)($iegjx) β†’ (A β†’ A))) }) ↦ ($iegjk : Nat) ↦ rec_{ Vec(Nat) ; A }(RecDataSym((vnil) (Nat)))(RecDataSym((vcons) (Nat)))
In [57]:
vfn.typ
Out[57]:
res56: Typ[U] = (A β†’ (∏($iegjx : Nat){ (Nat β†’ (Vec(Nat)($iegjx) β†’ (A β†’ A))) } β†’ ∏($iegjk : Nat){ (Vec(Nat)($iegjk) β†’ A) }))
In [58]:
vfn("a" :: A)
Out[58]:
res57: Term = (RecDataSym((vcons) (Nat)) : ∏($iegjx : Nat){ (Nat β†’ (Vec(Nat)($iegjx) β†’ (A β†’ A))) }) ↦ ($iegjk : Nat) ↦ rec_{ Vec(Nat) ; A }(a)(RecDataSym((vcons) (Nat)))
In [59]:
val a = "a" :: A
vfn(a).typ
Out[59]:
a: Term = a
res58_1: Typ[U] = (∏($iegjx : Nat){ (Nat β†’ (Vec(Nat)($iegjx) β†’ (A β†’ A))) } β†’ ∏($iegjk : Nat){ (Vec(Nat)($iegjk) β†’ A) })
In [60]:
val B = "B" :: Type
vecAStr.recOpt(Vec(A), B)
Out[60]:
B: Typ[Term] = B
res59_1: Option[Term] = Some(
  (RecDataSym((vnil) (A)) : B) ↦ (RecDataSym((vcons) (A)) : ∏($ieihf : Nat){ (A β†’ (Vec(A)($ieihf) β†’ (B β†’ B))) }) ↦ ($ieigs : Nat) ↦ rec_{ Vec(A) ; B }(RecDataSym((vnil) (A)))(RecDataSym((vcons) (A)))
)
In [61]:
vecStr.recOpt(Vec(A), B)
Out[61]:
res60: Option[Term] = Some(
  (RecDataSym((vnil) (A)) : B) ↦ (RecDataSym((vcons) (A)) : ∏($iejtz : Nat){ (A β†’ (Vec(A)($iejtz) β†’ (B β†’ B))) }) ↦ ($iejtm : Nat) ↦ rec_{ Vec(A) ; B }(RecDataSym((vnil) (A)))(RecDataSym((vcons) (A)))
)
In [62]:
vecStr.recOpt(Vec(B), Nat)
Out[62]:
res61: Option[Term] = Some(
  (RecDataSym((vnil) (B)) : Nat) ↦ (RecDataSym((vcons) (B)) : ∏($ielgu : Nat){ (B β†’ (Vec(B)($ielgu) β†’ (Nat β†’ Nat))) }) ↦ ($ielgh : Nat) ↦ rec_{ Vec(B) ; Nat }(RecDataSym((vnil) (B)))(RecDataSym((vcons) (B)))
)
In [63]:
val ok = vecStr.recOpt(Vec(A), Nat).get
Out[63]:
ok: Term = (RecDataSym((vnil) (A)) : Nat) ↦ (RecDataSym((vcons) (A)) : ∏($iemto : Nat){ (A β†’ (Vec(A)($iemto) β†’ (Nat β†’ Nat))) }) ↦ ($iemtb : Nat) ↦ rec_{ Vec(A) ; Nat }(RecDataSym((vnil) (A)))(RecDataSym((vcons) (A)))
In [64]:
val bok = ok.replace(A, B)
Out[64]:
bok: Term with Subs[Term] = (RecDataSym((vnil) (A)) : Nat) ↦ (RecDataSym((vcons) (A)) : ∏($iemto : Nat){ (B β†’ (Vec(B)($iemto) β†’ (Nat β†’ Nat))) }) ↦ ($iemtb : Nat) ↦ rec_{ Vec(B) ; Nat }(RecDataSym((vnil) (A)))(RecDataSym((vcons) (A)))
In [65]:
bok.typ
Out[65]:
res64: Typ[U] = (Nat β†’ (∏($iemto : Nat){ (B β†’ (Vec(B)($iemto) β†’ (Nat β†’ Nat))) } β†’ ∏($iemtb : Nat){ (Vec(B)($iemtb) β†’ Nat) }))
In [66]:
val nok = vecStr.recOpt(Vec(B), Nat).get
Out[66]:
nok: Term = (RecDataSym((vnil) (B)) : Nat) ↦ (RecDataSym((vcons) (B)) : ∏($ieoza : Nat){ (B β†’ (Vec(B)($ieoza) β†’ (Nat β†’ Nat))) }) ↦ ($ieoyn : Nat) ↦ rec_{ Vec(B) ; Nat }(RecDataSym((vnil) (B)))(RecDataSym((vcons) (B)))
In [67]:
vecAStr.subs(A, B).recOpt(Vec(B), Nat)
Out[67]:
res66: Option[Term] = Some(
  (RecDataSym((vnil) (B)) : Nat) ↦ (RecDataSym((vcons) (B)) : ∏($ieqlv : Nat){ (B β†’ (Vec(B)($ieqlv) β†’ (Nat β†’ Nat))) }) ↦ ($ieqli : Nat) ↦ rec_{ Vec(B) ; Nat }(RecDataSym((vnil) (B)))(RecDataSym((vcons) (B)))
)
In [68]:
vecAStr
vecAStr.subs(A, B)
Out[68]:
res67_0: ExstInducStrucs = IndConsSeqExst(
  Cons(
    (vnil) (A),
    IndexedIdShape(FuncTypFamily(Nat, IdTypFamily()), zero :: HNil),
    Cons(
      (vcons) (A),
      IndexedCnstDepFuncConsShape(
        Nat,
        provingground.induction.TypFamilyExst$IndexedConstructorShapeExst$$Lambda$4481/467783333@1ab80398
      ),
      Empty(Vec(A), FuncTypFamily(Nat, IdTypFamily()))
    )
  ),
  Vector(vnil(A), vcons(A))
)
res67_1: ExstInducStrucs = IndConsSeqExst(
  Cons(
    (vnil) (B),
    IndexedIdShape(FuncTypFamily(Nat, IdTypFamily()), zero :: HNil),
    Cons(
      (vcons) (B),
      IndexedCnstDepFuncConsShape(
        Nat,
        provingground.induction.IndexedConstructorShape$IndexedCnstDepFuncConsShape$$Lambda$4497/1709756592@183aba34
      ),
      Empty(Vec(B), FuncTypFamily(Nat, IdTypFamily()))
    )
  ),
  Vector(vnil(B), vcons(B))
)
In [69]:
val ndViT = mfd.nodeDist(tsV)(tg.Gen.inducFuncFoldedNode, 0.0001)
Out[69]:
ndViT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Map(
    FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$3843/1159594218@b419b14),
    provingground.learning.MonixFiniteDistribution$$Lambda$3947/871931955@22e705f3,
    0
  ),
  provingground.learning.MonixFiniteDistribution$$Lambda$3948/634189918@75f5ea88
)
In [70]:
val ndViD = ndViT.runSyncUnsafe()
Out[70]:
ndViD: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      ($kbvxl : Nat) ↦ induc_{ Vec(Vec(Nat)(zero)) ; (@a : Nat) ↦ (_ : Vec(Vec(Nat)(zero))(@a)) ↦ Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Vec(Nat)(zero)) ↦ (_ : Vec(Vec(Nat)(zero))(@a)) ↦ (_ : Nat) ↦ @a),
      0.005341200505608742
    ),
    Weighted(
      ($kbvxl : Nat) ↦ induc_{ Vec(Vec(Nat)(zero)) ; (@a : Nat) ↦ (_ : Vec(Vec(Nat)(zero))(@a)) ↦ Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Vec(Nat)(zero)) ↦ (_ : Vec(Vec(Nat)(zero))(@a)) ↦ (@b : Nat) ↦ @b),
      0.015572013135885547
    ),
    Weighted(
      ($kekth : Nat) ↦ induc_{ Vec(Vec(Nat)(succ(zero))) ; (@a : Nat) ↦ (_ : Vec(Vec(Nat)(succ(zero)))(@a)) ↦ Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Vec(Nat)(succ(zero))) ↦ (_ : Vec(Vec(Nat)(succ(zero)))(@a)) ↦ (@b : Nat) ↦ @b),
      0.013903223062656435
    ),
    Weighted(
      ($kekth : Nat) ↦ induc_{ Vec(Vec(Nat)(succ(zero))) ; (@a : Nat) ↦ (_ : Vec(Vec(Nat)(succ(zero)))(@a)) ↦ Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Vec(Nat)(succ(zero))) ↦ (_ : Vec(Vec(Nat)(succ(zero)))(@a)) ↦ (_ : Nat) ↦ @a),
      0.004768805510491157
    ),
    Weighted(
      ($kekth : Nat) ↦ induc_{ Vec(Vec(Nat)(succ(zero))) ; (@a : Nat) ↦ (_ : Vec(Vec(Nat)(succ(zero)))(@a)) ↦ Nat }(zero)((@a : Nat) ↦ (_ : Vec(Nat)(succ(zero))) ↦ (_ : Vec(Vec(Nat)(succ(zero)))(@a)) ↦ (_ : Nat) ↦ zero),
      0.002736225125668421
    ),
    Weighted(
      ($kbvxl : Nat) ↦ induc_{ Vec(Vec(Nat)(zero)) ; (@a : Nat) ↦ (_ : Vec(Vec(Nat)(zero))(@a)) ↦ Nat }(succ(zero))((@a : Nat) ↦ (_ : Vec(Nat)(zero)) ↦ (_ : Vec(Vec(Nat)(zero))(@a)) ↦ (_ : Nat) ↦ zero),
      0.001994646243547729
    ),
    Weighted(
      ($kbvxl : Nat) ↦ induc_{ Vec(Vec(Nat)(zero)) ; (@a : Nat) ↦ (_ : Vec(Vec(Nat)(zero))(@a)) ↦ Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Vec(Nat)(zero)) ↦ (_ : Vec(Vec(Nat)(zero))(@a)) ↦ (_ : Nat) ↦ succ(@a)),
      0.005341200505608741
    ),
    Weighted(
      ($kbvxl : Nat) ↦ induc_{ Vec(Vec(Nat)(zero)) ; (@a : Nat) ↦ (_ : Vec(Vec(Nat)(zero))(@a)) ↦ Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Vec(Nat)(zero)) ↦ (_ : Vec(Vec(Nat)(zero))(@a)) ↦ (@b : Nat) ↦ succ(@b)),
      0.015572013135885547
...
In [71]:
ndViD.map(_.typ).flatten
Out[71]:
res70: FiniteDistribution[Typ[U] forSome { type U >: x$1 <: Term with Subs[U]; val x$1: Term }] = FiniteDistribution(
  Vector(
    Weighted(∏($kqfyf : Nat){ ∏(_ : Vec(Nat)($kqfyf)){ Nat } }, 0.1993333487394483),
    Weighted(
      ∏($kekth : Nat){ ∏(_ : Vec(Vec(Nat)(succ(zero)))($kekth)){ Nat } },
      0.19370506660290493
    ),
    Weighted(∏($kbvxl : Nat){ ∏(_ : Vec(Vec(Nat)(zero))($kbvxl)){ Nat } }, 0.33079458674518497),
    Weighted(∏($kqplh : Nat){ ∏(_ : Vec(Nat)($kqplh)){ Vec(Nat)(zero) } }, 0.057974720772424645)
  )
)
In [72]:
val tgVT = mfd.nodeDist(tsV)(tg.Gen.codomainNode(Vec(Nat)(succ(zero))), 0.0001)
Out[72]:
tgVT: monix.eval.Task[FiniteDistribution[Term]] = Map(
  FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$3843/1159594218@b91b64b),
  provingground.learning.MonixFiniteDistribution$$Lambda$4641/1735864579@5a1aec2a,
  0
)
In [73]:
val tgVD = tgVT.runSyncUnsafe()
Out[73]:
tgVD: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      ($rvqmb : Nat) ↦ ($rvqmc : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)($rvqmb)($rvqmc),
      0.154700715184154
    ),
    Weighted(
      (_ : Nat) ↦ (_ : Nat) ↦ ($rvqrt : Nat) ↦ ($rvqru : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)($rvqrt)($rvqru),
      5.384663092456733E-4
    ),
    Weighted(
      ((__1 , __2) : Nat×𝒰 ) ↦ ($rvqxw : Nat) ↦ ($rvqxx : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)($rvqxw)($rvqxx),
      5.53851060938407E-4
    ),
    Weighted(($rbnts : Nat) ↦ vcons(Nat)(zero)($rbnts)(vnil(Nat)), 0.006797579553347722),
    Weighted(
      ((__1 , __2) : NatΓ—Nat) ↦ ($rvrnz : Nat) ↦ ($rvroa : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)($rvrnz)($rvroa),
      5.53851060938407E-4
    ),
    Weighted(
      (_ : 𝒰 ) ↦ ($rvsbu : Nat) ↦ ($rvsbv : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)($rvsbu)($rvsbv),
      0.0024826895435484143
    ),
    Weighted(
      ($rvsht : Nat) ↦ ($rvshu : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)($rvsht)($rvshu),
      0.035186122901365476
    ),
    Weighted(
      (_ : Nat) ↦ ($rvsnu : Nat) ↦ ($rvsnv : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)($rvsnu)($rvsnv),
      0.006054855390143681
    ),
    Weighted(
      (_ : Vec(Nat)(zero)) ↦ ($rvstl : Nat) ↦ ($rvstm : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)($rvstl)($rvstm),
      0.004305240247577042
    ),
    Weighted(
      (_ : Nat) ↦ ($rvszu : Nat) ↦ ($rvszv : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)($rvszu)($rvszv),
      7.889616252683857E-4
    ),
    Weighted(
      (_ : Nat) ↦ ($rvtfn : Nat) ↦ ($rvtfo : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)($rvtfn)($rvtfo),
      0.00846161343100344
    ),
    Weighted((@a : ∏(@a : 𝒰 ){ @a }) ↦ @a(Vec(Nat)(succ(zero))), 0.0015322303242512776),
    Weighted(($rvtoh : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)(zero)($rvtoh), 0.014482464400612847),
...
In [74]:
tgVD.map(_.typ).flatten
Out[74]:
res73: FiniteDistribution[Typ[U] forSome { type U >: x$1 <: Term with Subs[U]; val x$1: Term }] = FiniteDistribution(
  Vector(
    Weighted(((Nat β†’ Nat) β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero))))), 9.167189974152944E-4),
    Weighted(((𝒰  β†’ Nat) β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero))))), 6.951785730399314E-4),
    Weighted(
      (∏(@a : 𝒰 ){ @a } β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero))))),
      5.958673483199414E-4
    ),
    Weighted((Nat×𝒰  β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero))))), 5.53851060938407E-4),
    Weighted((NatΓ—Nat β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero))))), 5.53851060938407E-4),
    Weighted((𝒰  β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero))))), 0.014261555852124554),
    Weighted((Nat β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero))))), 0.015305430446415507),
    Weighted(
      (Vec(Nat)(zero) β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero))))),
      0.012657264708131517
    ),
    Weighted(((Nat β†’ 𝒰 ) β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero))))), 9.167189974152944E-4),
    Weighted(((𝒰  β†’ 𝒰 ) β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero))))), 6.951785730399314E-4),
    Weighted((Vec(Nat)(succ(zero)) β†’ Vec(Nat)(succ(zero))), 0.002352933170596089),
    Weighted((Nat β†’ Vec(Nat)(succ(zero))), 0.006797579553347722),
    Weighted((∏(@a : 𝒰 ){ @a } β†’ Vec(Nat)(succ(zero))), 0.0015322303242512776),
    Weighted((Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero))), 0.032468944751582414),
    Weighted((Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero)))), 0.908619763963952),
    Weighted((Nat β†’ (Nat β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero)))))), 5.384663092456733E-4),
    Weighted((Nat β†’ (𝒰  β†’ (Nat β†’ (Vec(Nat)(zero) β†’ Vec(Nat)(succ(zero)))))), 5.384663092456733E-4)
  )
)
In [75]:
Unify.targetCodomain(vcons, Vec(Nat)(succ(zero)))
Out[75]:
res74: Option[Term] = Some(
  ($sbtij : Nat) ↦ ($sbtik : Vec(Nat)(zero)) ↦ vcons(Nat)(zero)($sbtij)($sbtik)
)
In [76]:
Unify.unify(vcons.typ, Vec(Nat)(succ(zero)), (t) => false)
Out[76]:
res75: Option[Map[Term, Term]] = None
In [77]:
val tgtVT = mfd.nodeDist(tsV)(tg.Gen.foldedTargetFunctionNode(Vec(Nat)(succ(zero))), 0.001)
Out[77]:
tgtVT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Map(
    FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$3843/1159594218@13ecace6),
    provingground.learning.MonixFiniteDistribution$$Lambda$3961/1080967416@29133795,
    0
  ),
  provingground.learning.MonixFiniteDistribution$$Lambda$3962/1398506810@c43895c
)
In [78]:
val tgtVD = tgtVT.runSyncUnsafe()
Out[78]:
tgtVD: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(vcons(Nat)(zero)(zero)(vnil(Nat)), 0.3632480936136992),
    Weighted(vcons(Nat)(zero)(succ(zero))(vnil(Nat)), 0.5637928430189322),
    Weighted(vcons(Nat)(zero)(zero)(vnil(Nat)), 0.006977063857306793)
  )
)
In [79]:
val tgtNT = mfd.nodeDist(tsV)(tg.Gen.foldedTargetFunctionNode(Nat ->: Nat), 0.001)
Out[79]:
tgtNT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Map(
    FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$3843/1159594218@4b240dd8),
    provingground.learning.MonixFiniteDistribution$$Lambda$3961/1080967416@29133795,
    0
  ),
  provingground.learning.MonixFiniteDistribution$$Lambda$3962/1398506810@bda5192
)
In [80]:
val tgtND = tgtNT.runSyncUnsafe()
Out[80]:
tgtND: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(succ, 0.033392963625521764),
    Weighted(succ, 0.8067978533094812),
    Weighted((@a : Nat) ↦ @a, 0.08586762075134169),
    Weighted((_ : Nat) ↦ zero, 0.033392963625521764),
    Weighted(succ, 0.0071556350626118094),
    Weighted(succ, 0.033392963625521764)
  )
)
In [81]:
val node = tg.Gen.foldFuncTarget(succ, Nat, Terms).get
Out[81]:
node: GeneratorNode[Term] = FlatMapOpt(
  AtCoord(TermsWithTyp, Nat :: HNil),
  provingground.learning.TermGeneratorNodes$$Lambda$4685/213507035@38fcdd8f,
  Terms
)
In [82]:
val fd = mfd.nodeDist(tsV)(node, 0.0001).runSyncUnsafe()
Out[82]:
fd: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(succ(succ(succ(succ(zero)))), 7.64905568259782E-4),
    Weighted(succ(zero), 0.4665450047022078),
    Weighted(succ(succ(zero)), 0.3090352816016098),
    Weighted(succ(succ(succ(zero))), 0.22365480812792266)
  )
)
In [83]:
val nfd = mfd.nodeDist(tsV)(tg.Gen.codomainNode(Nat ->: Nat), 0.001).runSyncUnsafe()
Out[83]:
nfd: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted((_ : 𝒰 ) ↦ succ, 0.033392963625521764),
    Weighted(succ, 0.8067978533094812),
    Weighted((@a : Nat) ↦ @a, 0.08586762075134169),
    Weighted((_ : Nat) ↦ zero, 0.033392963625521764),
    Weighted((@a : (Nat β†’ Nat)) ↦ @a, 0.0071556350626118094),
    Weighted((_ : Nat) ↦ succ, 0.033392963625521764)
  )
)
In [84]:
val ffd = mfd.varDist(tsV)(funcForCod(Nat ->: Nat), 0.0001).runSyncUnsafe()
Out[84]:
ffd: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted((_ : (𝒰  β†’ Nat)) ↦ succ, 8.637156053595128E-4),
    Weighted((_ : (Nat β†’ Nat)) ↦ succ, 0.0011389656334411162),
    Weighted((_ : Nat) ↦ (_ : 𝒰 ) ↦ succ, 6.690104849205625E-4),
    Weighted((_ : Nat) ↦ (_ : Nat) ↦ zero, 6.690104849205625E-4),
    Weighted((_ : 𝒰 ) ↦ succ, 0.011731269079538992),
    Weighted(succ, 0.8239928126289577),
    Weighted((@a : Nat) ↦ (_ : Nat) ↦ @a, 0.0017203126755100185),
    Weighted((_ : Nat) ↦ (@b : Nat) ↦ @b, 0.002457589536442883),
    Weighted((@a : Nat) ↦ @a, 0.07893885136777896),
    Weighted((_ : Vec(Nat)(zero)) ↦ (@a : Nat) ↦ @a, 0.0021378364357880967),
    Weighted((_ : Nat) ↦ (_ : Nat) ↦ succ, 6.690104849205625E-4),
    Weighted((_ : Nat) ↦ zero, 0.030058554794242222),
    Weighted((_ : ∏(@a : 𝒰 ){ @a }) ↦ succ, 7.403276617367255E-4),
    Weighted((_ : Vec(Nat)(zero)) ↦ succ, 0.00914518919753797),
    Weighted((_ : 𝒰 ) ↦ (@a : Nat) ↦ @a, 0.001919662213015471),
    Weighted((@a : ∏(@a : 𝒰 ){ @a }) ↦ @a((Nat β†’ Nat)), 0.0019036997016087225),
    Weighted((_ : Nat) ↦ succ(zero), 0.004038568788091896),
    Weighted((_ : (𝒰  β†’ 𝒰 )) ↦ succ, 8.637156053595128E-4),
    Weighted((_ : (Nat β†’ 𝒰 )) ↦ succ, 0.0011389656334411162),
    Weighted((@a : Nat) ↦ succ(@a), 0.010384891169379162),
    Weighted((@a : (Nat β†’ Nat)) ↦ @a, 0.0029287687717057275),
    Weighted((_ : Nat) ↦ succ, 0.01051302190589456),
    Weighted(((__1 , __2) : Nat×𝒰 ) ↦ succ, 6.881250702040076E-4),
    Weighted(((__1 , __2) : NatΓ—Nat) ↦ succ, 6.881250702040076E-4)
  )
)
In [92]:
val indTargT = mfd.nodeDist(ts1)(tg.Gen.targetInducNode(Nat ->: Nat), 0.0001)
Out[92]:
indTargT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Map(
    FlatMap(Async(<function2>, true, true, true), monix.eval.Task$$Lambda$3843/1159594218@2c416bb0),
    provingground.learning.MonixFiniteDistribution$$Lambda$3961/1080967416@29133795,
    0
  ),
  provingground.learning.MonixFiniteDistribution$$Lambda$3962/1398506810@360b754f
)
In [93]:
indTargT.runSyncUnsafe()
Out[93]:
res92: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((@a : Nat) ↦ (_ : Nat) ↦ succ(@a)),
      0.016348855278431905
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)),
      0.02335550754061701
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((_ : Nat) ↦ (@b : Nat) ↦ succ(@b)),
      0.027912269926652758
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((@a : Nat) ↦ (_ : Nat) ↦ succ(@a)),
      0.019082732126670676
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((_ : Nat) ↦ (_ : Nat) ↦ succ(zero)),
      0.008905274992446316
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((@a : Nat) ↦ (_ : Nat) ↦ succ(succ(@a))),
      0.006652850436204436
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((_ : Nat) ↦ (@b : Nat) ↦ succ(succ(@b))),
      0.022522944234461998
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(zero))((_ : Nat) ↦ (_ : Nat) ↦ zero),
      0.007583299795560589
    ),
    Weighted(induc_{ Nat ; (_ : Nat) ↦ Nat }(zero)((_ : Nat) ↦ succ), 0.23445459080365516),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((_ : Nat) ↦ (_ : Nat) ↦ succ(zero)),
      0.007629465796601556
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(zero)((_ : Nat) ↦ (_ : Nat) ↦ succ(zero)),
      0.011870916539622063
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(zero)))((_ : Nat) ↦ (_ : Nat) ↦ zero),
      0.0030681266609904924
    ),
    Weighted(
      induc_{ Nat ; (_ : Nat) ↦ Nat }(succ(succ(succ(zero))))((@a : Nat) ↦ (_ : Nat) ↦ succ(@a)),
...
In [ ]: