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.