Testing skolemizationΒΆ

We test skolemizing types and mapping a term from the skolemized type.

In [1]:
import $cp.bin.`provingground-core-jvm-16c05447f5.fat.jar`
import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}
Out[1]:
import $cp.$                                              

import provingground._ , interface._, HoTT._, learning._
In [2]:
val lp = LocalProver(TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type)))
Out[2]:
lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
    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,
    0.0,
    0.0,
    OrElse(
      OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
      <function1>
    )
  ),
  1.0E-4,
  None,
  12 minutes,
  1.01,
  1.0,
...
In [3]:
val typsT = lp.varDist(TermRandomVars.Typs)
Out[3]:
typsT: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Map(
  FlatMap(
    Async(<function2>, true, true, true),
    monix.eval.Task$$Lambda$2532/391230082@40f1ded4
  ),
  scala.Function1$$Lambda$332/412925308@7cfc1c81,
  1
)
In [4]:
import monix.execution.Scheduler.Implicits.global
val typs = typsT.runSyncUnsafe()
Out[4]:
import monix.execution.Scheduler.Implicits.global

typs: FiniteDistribution[Typ[Term]] = FiniteDistribution(
  Vector(
    Weighted((∏(@a : 𝒰 ){ @a } β†’ 𝒰 )×𝒰 , 2.864303616183315E-4),
    Weighted((𝒰  β†’ 𝒰 )×𝒰 , 0.0030964747095065226),
    Weighted((𝒰 ×𝒰  β†’ 𝒰 )×𝒰 , 3.3416875522138676E-4),
    Weighted(((𝒰  β†’ 𝒰 ) β†’ 𝒰 )×𝒰 , 6.683375104427735E-4),
    Weighted((𝒰  β†’ 𝒰 )Γ—βˆ(@a : 𝒰 ){ @a }, 1.5482373547532613E-4),
    Weighted(βˆ‘(@a : 𝒰 ){ @aΓ—@a }, 2.531792092091293E-4),
    Weighted((𝒰  β†’ βˆ‘(@b : 𝒰 ){ @b }), 8.854437201954419E-4),
    Weighted(𝒰 , 0.8421052631578946),
    Weighted(∏(@a : 𝒰 ){ @a×𝒰  }, 8.854437201954417E-4),
    Weighted((𝒰  β†’ 𝒰 )×𝒰 ×𝒰 , 1.8062769138788048E-4),
    Weighted(βˆ‘(@a : 𝒰 ){ @a }, 0.010127168368365172),
    Weighted((𝒰  β†’ (𝒰  β†’ 𝒰 ))×𝒰 , 3.097764907302151E-4),
    Weighted(βˆ‘(@a : 𝒰 ){ (@a β†’ @a) }, 4.7897690533021465E-4),
    Weighted(βˆ‘(@a : 𝒰 ){ (𝒰  β†’ @a) }, 7.823289453726841E-4),
    Weighted(∏(@a : 𝒰 ){ @a }×𝒰 , 0.0016256492224909244),
    Weighted(βˆ‘(@a : 𝒰 ){ 𝒰 Γ—@a }, 4.135260417082446E-4),
    Weighted(βˆ‘(@a : 𝒰 ){ @a }×𝒰 , 9.426551453260014E-4),
    Weighted(𝒰 Γ—βˆ‘(@b : 𝒰 ){ @b }, 5.907514881546351E-4),
    Weighted(𝒰 ×𝒰 Γ—(𝒰  β†’ 𝒰 ), 2.2980150308942325E-4),
    Weighted(𝒰 ×𝒰 , 0.023630059526185403),
    Weighted((𝒰 ×𝒰  β†’ ∏(@a : 𝒰 ){ @a }), 1.5482373547532618E-4),
    Weighted(∏(@a : 𝒰 ){ (@a β†’ @a) }, 6.79803857197287E-4),
    Weighted(∏(@a : 𝒰 ){ ((𝒰  β†’ 𝒰 ) β†’ @a) }, 1.2954040167703856E-4),
    Weighted(∏(@a : 𝒰 ){ (𝒰  β†’ @a) }, 0.0011103463000889024),
    Weighted((𝒰  β†’ ∏(@b : 𝒰 ){ @b }), 0.0015862090001270033),
    Weighted(((𝒰  β†’ 𝒰 ) β†’ ∏(@a : 𝒰 ){ @a }), 2.718085193921044E-4),
    Weighted((∏(@a : 𝒰 ){ @a }×𝒰  β†’ 𝒰 ), 2.8643036161833153E-4),
    Weighted((βˆ‘(@a : 𝒰 ){ @a } β†’ 𝒰 ), 0.0016256492224909246),
    Weighted(((𝒰  β†’ 𝒰 )×𝒰  β†’ 𝒰 ), 6.683375104427735E-4),
    Weighted((𝒰  β†’ 𝒰 ), 0.055272207947044544),
    Weighted((𝒰 ×𝒰  β†’ 𝒰 ), 0.003096474709506523),
    Weighted((∏(@a : 𝒰 ){ (𝒰  β†’ @a) } β†’ 𝒰 ), 2.3307580537872962E-4),
    Weighted(((𝒰  β†’ ∏(@b : 𝒰 ){ @b }) β†’ 𝒰 ), 3.329654362553281E-4),
    Weighted(((𝒰  β†’ 𝒰 ) β†’ 𝒰 ), 0.005436170387842089),
    Weighted(((βˆ‘(@a : 𝒰 ){ @a } β†’ 𝒰 ) β†’ 𝒰 ), 2.807017543859649E-4),
    Weighted(((𝒰 ×𝒰  β†’ 𝒰 ) β†’ 𝒰 ), 6.549707602339181E-4),
    Weighted((((𝒰  β†’ 𝒰 ) β†’ 𝒰 ) β†’ 𝒰 ), 0.0013099415204678362),
...
In [5]:
import scala.util._
def skolemCheck(typ: Typ[Term]) = {
    val sk = skolemize(typ)
    val x = sk.Var
    (typ, sk, Try(fromSkolemized(typ)(x)))
}
Out[5]:
import scala.util._

defined function skolemCheck
In [6]:
val checklist = typs.supp.map(skolemCheck)
Out[6]:
checklist: Vector[(Typ[Term], Typ[Term], Try[Term])] = Vector(
  (
    (∏(@a : 𝒰 ){ @a } β†’ 𝒰 )×𝒰 ,
    (∏(@a : 𝒰 ){ @a } β†’ 𝒰 )×𝒰 ,
    Success((($hkd : ∏(@a : 𝒰 ){ @a }) ↦ $hjy_1($hkd) , $hjy_2))
  ),
  (
    (𝒰  β†’ 𝒰 )×𝒰 ,
    (𝒰  β†’ 𝒰 )×𝒰 ,
    Success((($hln : 𝒰 ) ↦ $hlk_1($hln) , $hlk_2))
  ),
  (
    (𝒰 ×𝒰  β†’ 𝒰 )×𝒰 ,
    (𝒰 ×𝒰  β†’ 𝒰 )×𝒰 ,
    Success(
      (((`$hlv_1 , $hlv_2) : 𝒰 ×𝒰 ) ↦ $hls_1((`$hlv_1 , $hlv_2)) , $hls_2)
    )
  ),
  (
    ((𝒰  β†’ 𝒰 ) β†’ 𝒰 )×𝒰 ,
    ((𝒰  β†’ 𝒰 ) β†’ 𝒰 )×𝒰 ,
    Success((($hmf : (𝒰  β†’ 𝒰 )) ↦ $hma_1($hmf) , $hma_2))
  ),
  (
    (𝒰  β†’ 𝒰 )Γ—βˆ(@a : 𝒰 ){ @a },
    (𝒰  β†’ 𝒰 )Γ—βˆ(@a : 𝒰 ){ @a },
    Success((($hnq : 𝒰 ) ↦ $hnm_1($hnq) , (@a : 𝒰 ) ↦ $hnm_2(@a)))
  ),
  (
    βˆ‘(@a : 𝒰 ){ @aΓ—@a },
    βˆ‘(@a : 𝒰 ){ @aΓ—@a },
    Success(($hnz_1 , ($hnz_2_1 , $hnz_2_2)))
  ),
  (
    (𝒰  β†’ βˆ‘(@b : 𝒰 ){ @b }),
    βˆ‘($hob : (𝒰  β†’ 𝒰 )){ ∏($hoa : 𝒰 ){ $hob($hoa) } },
    Success(($jtr : 𝒰 ) ↦ ($hot_1($jtr) , $hot_2($jtr)))
  ),
  (𝒰 , 𝒰 , Success($kql)),
...
In [7]:
checklist.filter(_._3.isFailure)
Out[7]:
res6: Vector[(Typ[Term], Typ[Term], Try[Term])] = Vector()
In [8]:
val lp1 = LocalProver(TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))).sharpen(10).asInstanceOf[LocalProver]
Out[8]:
lp1: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
    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,
    0.0,
    0.0,
    OrElse(
      OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
      <function1>
    )
  ),
  1.0E-5,
  None,
  12 minutes,
  1.01,
  1.0,
...
In [9]:
import TermRandomVars.Typs
val typs1T = lp1.varDist(Typs).memoize
Out[9]:
import TermRandomVars.Typs

typs1T: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Async(
  <function2>,
  false,
  true,
  true
)
In [10]:
val typs1 = typs1T.runSyncUnsafe()
Out[10]:
typs1: FiniteDistribution[Typ[Term]] = FiniteDistribution(
  Vector(
    Weighted(((𝒰 ×𝒰  β†’ 𝒰 ) β†’ 𝒰 )×𝒰 , 3.5165091915152586E-5),
    Weighted((((𝒰  β†’ 𝒰 ) β†’ 𝒰 ) β†’ 𝒰 )×𝒰 , 7.033018383030517E-5),
    Weighted((𝒰 ×𝒰  β†’ 𝒰 )×𝒰 , 1.8562156889144032E-4),
    Weighted((βˆ‘(@a : 𝒰 ){ @a } β†’ 𝒰 )×𝒰 , 9.919705032781848E-5),
    Weighted(((𝒰  β†’ 𝒰 )×𝒰  β†’ 𝒰 )×𝒰 , 3.8576630683040526E-5),
    Weighted((𝒰  β†’ 𝒰 )×𝒰 , 0.0019893019971860145),
    Weighted((∏(@a : 𝒰 ){ @a } β†’ 𝒰 )×𝒰 , 1.7106956720958893E-4),
    Weighted(((𝒰  β†’ (𝒰  β†’ 𝒰 )) β†’ 𝒰 )×𝒰 , 3.2598256418271675E-5),
    Weighted(((𝒰  β†’ 𝒰 ) β†’ 𝒰 )×𝒰 , 2.9180309971784887E-4),
    Weighted(((∏(@a : 𝒰 ){ @a } β†’ 𝒰 ) β†’ 𝒰 )×𝒰 , 3.014150735584507E-5),
    Weighted(∏(@a : 𝒰 ){ @aΓ—@a }×𝒰 , 2.6642437462312702E-5),
    Weighted((𝒰  β†’ (𝒰  β†’ βˆ‘(@c : 𝒰 ){ @c })), 5.7835540448263214E-5),
    Weighted(∏(@a : 𝒰 ){ (@a β†’ βˆ‘(@b : 𝒰 ){ @b }) }, 2.413188179929202E-5),
    Weighted(∏(@a : 𝒰 ){ @a }×𝒰 ×𝒰 , 4.9732549929650365E-5),
    Weighted(βˆ‘(@a : (𝒰  β†’ 𝒰 )){ ∏(@a : 𝒰 ){ @a(@a) } }, 4.241582083552271E-5),
    Weighted((𝒰  β†’ 𝒰 )Γ—βˆ(@a : 𝒰 ){ @a }, 7.634847750394084E-5),
    Weighted(βˆ‘(@a : 𝒰 ){ @aΓ—@a }, 1.493314624571734E-4),
    Weighted(βˆ‘(@a : 𝒰 ){ @a×𝒰 ×𝒰  }, 2.2199020648431023E-5),
    Weighted(∏(@a : 𝒰 ){ @aΓ—@a×𝒰  }, 1.8952021767169072E-5),
    Weighted((∏(@a : 𝒰 ){ @a } β†’ βˆ‘(@a : 𝒰 ){ @a }), 3.377252570160576E-5),
    Weighted((βˆ‘(@a : 𝒰 ){ @a } β†’ βˆ‘(@a : 𝒰 ){ @a }), 1.912316937487314E-4),
    Weighted((𝒰  β†’ βˆ‘(@b : 𝒰 ){ @b }), 6.164148653051663E-4),
    Weighted((𝒰 ×𝒰  β†’ βˆ‘(@a : 𝒰 ){ @a }), 4.973254992965036E-5),
    Weighted(((𝒰  β†’ 𝒰 ) β†’ βˆ‘(@a : 𝒰 ){ @a }), 8.929196560765703E-5),
    Weighted(βˆ‘(@a : 𝒰 ){ @a }×𝒰 ×𝒰 , 2.547169635705217E-5),
    Weighted(∏(@a : 𝒰 ){ βˆ‘(@a : (𝒰  β†’ 𝒰 )){ @a(@a) } }, 2.788673127756236E-5),
    Weighted(
      ∏(@a : (𝒰  β†’ 𝒰 )){ βˆ‘(@a : 𝒰 ){ @a(@a) } },
      4.9606647559809485E-5
    ),
    Weighted(βˆ‘(@a : 𝒰 ){ (@a β†’ 𝒰 )×𝒰  }, 4.4398041296862046E-5),
    Weighted((𝒰 Γ—(𝒰  β†’ 𝒰 ) β†’ 𝒰 Γ—(𝒰  β†’ 𝒰 )), 2.5196234752183232E-5),
    Weighted(∏(@a : 𝒰 ){ 𝒰 Γ—(@a β†’ 𝒰 ) }, 3.523838313327868E-5),
    Weighted((𝒰  β†’ 𝒰 Γ—(𝒰  β†’ 𝒰 )), 5.755602578435516E-5),
    Weighted(𝒰 , 0.8030625601428774),
...
In [11]:
val checklist1 = typs1.supp.map(skolemCheck)
Out[11]:
checklist1: Vector[(Typ[Term], Typ[Term], Try[Term])] = Vector(
  (
    ((𝒰 ×𝒰  β†’ 𝒰 ) β†’ 𝒰 )×𝒰 ,
    ((𝒰 ×𝒰  β†’ 𝒰 ) β†’ 𝒰 )×𝒰 ,
    Success((($hgjk : (𝒰 ×𝒰  β†’ 𝒰 )) ↦ $hgjf_1($hgjk) , $hgjf_2))
  ),
  (
    (((𝒰  β†’ 𝒰 ) β†’ 𝒰 ) β†’ 𝒰 )×𝒰 ,
    (((𝒰  β†’ 𝒰 ) β†’ 𝒰 ) β†’ 𝒰 )×𝒰 ,
    Success((($hglc : ((𝒰  β†’ 𝒰 ) β†’ 𝒰 )) ↦ $hgkv_1($hglc) , $hgkv_2))
  ),
  (
    (𝒰 ×𝒰  β†’ 𝒰 )×𝒰 ,
    (𝒰 ×𝒰  β†’ 𝒰 )×𝒰 ,
    Success(
      (((`$hgnw_1 , $hgnw_2) : 𝒰 ×𝒰 ) ↦ $hgnt_1((`$hgnw_1 , $hgnw_2)) , $hgnt_2)
    )
  ),
  (
    (βˆ‘(@a : 𝒰 ){ @a } β†’ 𝒰 )×𝒰 ,
    (βˆ‘(@a : 𝒰 ){ @a } β†’ 𝒰 )×𝒰 ,
    Success(
      (((`$hgoe_1 , `$hgoe_2) : βˆ‘(@a : 𝒰 ){ @a }) ↦ $hgob_1((`$hgoe_1 , `$hgoe_2)) , $hgob_2)
    )
  ),
  (
    ((𝒰  β†’ 𝒰 )×𝒰  β†’ 𝒰 )×𝒰 ,
    ((𝒰  β†’ 𝒰 )×𝒰  β†’ 𝒰 )×𝒰 ,
    Success(
      (((`$hgoo_1 , $hgoo_2) : (𝒰  β†’ 𝒰 )×𝒰 ) ↦ $hgol_1((`$hgoo_1 , $hgoo_2)) , $hgol_2)
    )
  ),
  (
    (𝒰  β†’ 𝒰 )×𝒰 ,
    (𝒰  β†’ 𝒰 )×𝒰 ,
    Success((($hgqs : 𝒰 ) ↦ $hgqp_1($hgqs) , $hgqp_2))
...
In [12]:
checklist1.filter(_._3.isFailure)
Out[12]:
res11: Vector[(Typ[Term], Typ[Term], Try[Term])] = Vector()
In [13]:
typs1.entropyVec.reverse
Out[13]:
res12: Vector[Weighted[Typ[Term]]] = Vector(
  Weighted(∏(@a : 𝒰 ){ (@aΓ—@a β†’ @a) }, 16.328049464425735),
  Weighted((𝒰  β†’ ((𝒰  β†’ 𝒰 )×𝒰  β†’ 𝒰 )), 16.274981046797063),
  Weighted(∏(@a : 𝒰 ){ 𝒰 Γ—@aΓ—@a }, 16.201861886580808),
  Weighted(βˆ‘(@a : 𝒰 ){ (𝒰 Γ—@a β†’ @a) }, 16.201668331065452),
  Weighted(βˆ‘(@a : 𝒰 ){ (𝒰  β†’ @a)Γ—@a }, 16.196110037830245),
  Weighted((𝒰  β†’ ((∏(@b : 𝒰 ){ @b } β†’ 𝒰 ) β†’ 𝒰 )), 16.14168993679603),
  Weighted(∏(@a : 𝒰 ){ (((@a β†’ 𝒰 ) β†’ 𝒰 ) β†’ 𝒰 ) }, 16.14168993679603),
  Weighted(∏(@a : 𝒰 ){ 𝒰 Γ—(@a β†’ @a) }, 16.014885166154972),
  Weighted(βˆ‘(@a : 𝒰 ){ (𝒰  β†’ (@a β†’ @a)) }, 16.014691610639616),
  Weighted(∏(@a : 𝒰 ){ (@a β†’ @a)Γ—@a }, 15.989883976537127),
  Weighted(βˆ‘(@a : 𝒰 ){ ((@a β†’ @a) β†’ @a) }, 15.98969042102177),
  Weighted((𝒰  β†’ βˆ‘(@b : 𝒰 ){ @bΓ—@b }), 15.985738820495456),
  Weighted(𝒰 Γ—βˆ(@b : 𝒰 ){ @bΓ—@b }, 15.985545264980098),
  Weighted(βˆ‘(@a : 𝒰 ){ 𝒰 ×𝒰 Γ—@a }, 15.973717616493797),
  Weighted(βˆ‘(@a : 𝒰 ){ 𝒰 Γ—@a×𝒰  }, 15.973717616493797),
  Weighted(∏(@a : 𝒰 ){ @aΓ—βˆ‘(@b : 𝒰 ){ @b } }, 15.947615527221352),
  Weighted(βˆ‘(@a : 𝒰 ){ (@a β†’ βˆ‘(@b : 𝒰 ){ @b }) }, 15.947421971705996),
  Weighted((𝒰  β†’ ((𝒰  β†’ 𝒰 ) β†’ 𝒰 )×𝒰 ), 15.936815558908455),
  Weighted(𝒰 Γ—(((𝒰  β†’ 𝒰 ) β†’ 𝒰 ) β†’ 𝒰 ), 15.9366220033931),
  Weighted(∏(@a : 𝒰 ){ (@a β†’ 𝒰 Γ—@a) }, 15.853273226256977),
  Weighted(𝒰 Γ—βˆ‘(@b : 𝒰 ){ (@b β†’ @b) }, 15.853142962167958),
  Weighted((𝒰  β†’ (𝒰 ×𝒰  β†’ 𝒰 ×𝒰 )), 15.827391406557368),
  Weighted(∏(@a : 𝒰 ){ (𝒰  β†’ @aΓ—@a) }, 15.814649754578422),
  Weighted(βˆ‘(@a : 𝒰 ){ @aΓ—βˆ(@b : 𝒰 ){ @b } }, 15.808729896007383),
  Weighted((𝒰  β†’ βˆ‘(@b : 𝒰 ){ 𝒰 Γ—@b }), 15.792492744818526),
  Weighted(∏(@a : 𝒰 ){ 𝒰 Γ—@a×𝒰  }, 15.792492744818526),
  Weighted(βˆ‘(@a : 𝒰 ){ (𝒰  β†’ @a×𝒰 ) }, 15.792299189303169),
  Weighted(𝒰 Γ—βˆ(@b : 𝒰 ){ 𝒰 Γ—@b }, 15.792299189303169),
  Weighted(((𝒰  β†’ (𝒰  β†’ 𝒰 )×𝒰 ) β†’ 𝒰 ), 15.781389148384108),
  Weighted(∏(@a : 𝒰 ){ @a×𝒰 Γ—@a }, 15.687288713751052),
  Weighted(∏(@a : 𝒰 ){ βˆ‘(@b : 𝒰 ){ @b }Γ—@a }, 15.687288713751052),
  Weighted(∏(@a : 𝒰 ){ @aΓ—@a×𝒰  }, 15.687288713751052),
  Weighted(βˆ‘(@a : 𝒰 ){ (@aΓ—@a β†’ 𝒰 ) }, 15.687095158235694),
  Weighted(βˆ‘(@a : 𝒰 ){ (@a×𝒰  β†’ @a) }, 15.687095158235694),
  Weighted(βˆ‘(@a : 𝒰 ){ (βˆ‘(@b : 𝒰 ){ @b } β†’ @a) }, 15.687095158235694),
  Weighted(
    (∏(@a : 𝒰 ){ (𝒰  β†’ @a) } β†’ ∏(@a : 𝒰 ){ (𝒰  β†’ @a) }),
    15.686860725001898
...
In [14]:
typs1.support.size
Out[14]:
res13: Int = 366

ConclusionΒΆ

After debugging, skolemization works in many cases.