notebook.community

Edit and run

Modus Ponens

This correctly scales up cutoff (but perhaps too much, we also scale within Pi and PiOpt)





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._

















In [3]:



    


val A = Type.sym
val B = Type.sym
val MP = A ~>: B ~>: (A ->: (A ->: B) ->: B)
val ts = TermState(FD.unif(Type), FD.unif(Type), goals = FD.unif(MP))
val tg = TermGenParams()
val mfeq = MonixFiniteDistributionEq(tg.nodeCoeffSeq)



    


















    
Out[3]:








A: Typ[Term] = SymbTyp(Name("A"), 0)
B: Typ[Term] = SymbTyp(Name("B"), 0)
MP: GenFuncTyp[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]] = PiDefn(
  SymbTyp(A, 0),
  PiDefn(
    SymbTyp(B, 0),
    FuncTyp(
      SymbTyp(A, 0),
      FuncTyp(FuncTyp(SymbTyp(A, 0), SymbTyp(B, 0)), SymbTyp(B, 0))
    )
  )
)
ts: TermState = TermState(
  FiniteDistribution(Vector(Weighted(Universe(0), 1.0))),
  FiniteDistribution(Vector(Weighted(Universe(0), 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(
      Weighted(
        PiDefn(
          SymbTyp(A, 0),
          PiDefn(
            SymbTyp(B, 0),
            FuncTyp(
              SymbTyp(A, 0),
              FuncTyp(FuncTyp(SymbTyp(A, 0), SymbTyp(B, 0)), SymbTyp(B, 0))
            )
          )
        ),
        1.0
      )
    )
  ),
  Empty
)
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
)
mfeq: MonixFiniteDistributionEq[TermState, Term] = MonixFiniteDistributionEq(
  Cons(
    BaseCons(
      BasePi(
        provingground.learning.RandomVarFamily$$Lambda$3554/221246939@4aa1ee39,
        FuncsWithDomain
      ),
      0.55,
      BaseCons(
        BasePi(
          provingground.learning.GeneratorNode$$Lambda$3557/663473340@6729cd9,
          FuncsWithDomain
        ),
        0.1,
        BaseCons(
          BasePi(
            provingground.learning.GeneratorNode$$Lambda$3557/663473340@5bb9a681,
            FuncsWithDomain
          ),
          0.1,
          BaseCons(
            BasePi(
              provingground.learning.GeneratorNode$$Lambda$3557/663473340@4c9bcba1,
              FuncsWithDomain
            ),
            0.1,
            BaseCons(
              BasePi(
                provingground.learning.TermGeneratorNodes$$Lambda$3548/391798791@67b57543,
                FuncsWithDomain
              ),
              0.1,
              Target(FuncsWithDomain)
            )
          )
        )
...

















In [4]:



    


import TermRandomVars._
val getMPhard = mfeq.varDist(ts)(Terms, 0.0001)



    


















    
Out[4]:








import TermRandomVars._

getMPhard: monix.eval.Task[(FiniteDistribution[Term], Set[GeneratorVariables.EquationTerm])] = FlatMap(
  Async(<function2>, true, true, true),
  monix.eval.Task$$Lambda$3706/1986317742@217b0f83
)

















In [5]:



    


import monix.execution.Scheduler.Implicits.global 
val (fd, eqs) = getMPhard.runSyncUnsafe()



    


















    
Out[5]:








import monix.execution.Scheduler.Implicits.global 

fd: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(
      LambdaFixed(
        PiSymbolicFunc(Name("_"), SymbTyp(@a, 0), SymbTyp(@a, 0)),
        LambdaFixed(SymbTyp(Name("_"), 0), Universe(0))
      ),
      2.489207011819105E-4
    ),
    Weighted(
      LambdaFixed(
        SymbTyp(Name("_"), 0),
        LambdaFixed(
          PiSymbolicFunc(Name("_"), SymbTyp(@b, 0), SymbTyp(@b, 0)),
          Universe(0)
        )
      ),
      1.4161641559025961E-4
    ),
    Weighted(
      LambdaFixed(
        PairTerm(
          SymbTyp(LeftProjSym(Name("_")), 0),
          SymbolicFunc(RightProjSym(Name("_")), Universe(0), Universe(0))
        ),
        Universe(0)
      ),
      2.3119896721372646E-4
    ),
    Weighted(
      LambdaFixed(
        PairTerm(
          SymbTyp(LeftProjSym(Name("_")), 0),
          SymbTyp(RightProjSym(Name("_")), 0)
        ),
        LambdaFixed(SymbTyp(Name("_"), 0), Universe(0))
      ),
      3.1505650767257745E-4
    ),
...
eqs: Set[GeneratorVariables.EquationTerm] = Set(
  EquationTerm(
    FinalVal(
      Elem(ProdTyp(Universe(0), FuncTyp(Universe(0), Universe(0))), Typs)
    ),
    Product(
      Coeff(
        FlatMap(
          Typs,
          provingground.learning.TermGeneratorNodes$$Lambda$3550/841967481@1bb34c77,
          Typs
        ),
        Typs
      ),
      FinalVal(
        InIsle(
          Elem(FuncTyp(Universe(0), Universe(0)), Typs),
          SymbTyp(Name("@a"), 0),
          Island(Typs, ConstRandVar(Typs), AddVar(Universe(0), 0.3), Sigma, InIsle)
        )
      )
    )
  ),
  EquationTerm(
    InitialVal(
      InIsle(
        InIsle(
          Elem(Universe(0), Typs),
          SymbTyp(Name("@b"), 0),
          Island(Typs, ConstRandVar(Typs), AddVar(Universe(0), 0.3), Sigma, InIsle)
        ),
        SymbTyp(Name("@a"), 0),
        Island(Typs, ConstRandVar(Typs), AddVar(Universe(0), 0.3), Pi, InIsle)
      )
    ),
    Product(
      IsleScale(SymbTyp(Name("@b"), 0), Elem(Universe(0), Typs)),
      InitialVal(
...

















In [6]:



    


repl.pprinter.bind(translation.FansiShow.fansiPrint)
fd.filter(_.typ == MP)



    


















    
Out[6]:








res5_1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted((@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a), 0.03928111738491071)
  )
)

















In [7]:



    


, Expression._
val mpEqs = eqs.collect{case eq @ EquationTerm(FinalVal(Elem(t : Term, _)), _) if t.typ == MP => eq}



    


















    
Out[7]:








import GeneratorVariables._

mpEqs: Set[EquationTerm] = Set(
  EquationTerm(
    FinalVal(Elem((@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a), Terms)),
    Product(
      Product(
        Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
        FinalVal(Elem(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, TargetTyps))
      ),
      FinalVal(
        Elem(
          (@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
          AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil)
        )
      )
    )
  ),
  EquationTerm(
    FinalVal(
      Elem(
        (@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
        AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil)
      )
    ),
    Product(
      Coeff(
        Island(
          AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil),
          PiOutput(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }),
          AddVar(𝒰 , 0.3),
          Lambda,
          InIsle
        ),
        AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil)
      ),
      FinalVal(
        InIsle(
          Elem(
            (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
            AtCoord(TermsWithTyp, ∏(B : 𝒰 ){ (@a → ((@a → B) → B)) } :: HNil)
          ),
          @a,
          Island(
            AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil),
            PiOutput(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }),
            AddVar(𝒰 , 0.3),
            Lambda,
            InIsle
          )
        )
...

















In [8]:



    


val ats = mpEqs.map(_.rhs).flatMap(Expression.atoms)



    


















    
Out[8]:








ats: Set[Expression] = Set(
  Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
  FinalVal(
    Elem(
      (@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
      AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil)
    )
  ),
  Coeff(
    Island(
      AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil),
      PiOutput(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }),
      AddVar(𝒰 , 0.3),
      Lambda,
      InIsle
    ),
    AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil)
  ),
  FinalVal(Elem(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, TargetTyps)),
  FinalVal(
    InIsle(
      Elem(
        (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
        AtCoord(TermsWithTyp, ∏(B : 𝒰 ){ (@a → ((@a → B) → B)) } :: HNil)
      ),
      @a,
      Island(
        AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil),
        PiOutput(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }),
        AddVar(𝒰 , 0.3),
        Lambda,
        InIsle
      )
    )
  )
)

















In [9]:



    


val coeffs = ats.collect{case cf @ Coeff(_, _) => cf}.toVector



    


















    
Out[9]:








coeffs: Vector[Coeff[Any]] = Vector(
  Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
  Coeff(
    Island(
      AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil),
      PiOutput(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }),
      AddVar(𝒰 , 0.3),
      Lambda,
      InIsle
    ),
    AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil)
  )
)

















In [10]:



    


coeffs.map(_.get(tg.nodeCoeffSeq))



    


















    
Out[10]:








res9: Vector[Option[Double]] = Vector(Some(0.05), Some(0.485))

















In [11]:



    


coeffs.map(_.expand)



    


















    
Out[11]:








res10: Vector[RandomVarFamily[_, Any] forSome { type _ <: shapeless.HList }] = Vector(
  Terms,
  TermsWithTyp
)

















In [12]:



    


tg.nodeCoeffSeq.find(TermsWithTyp)



    


















    
Out[12]:








res11: Option[NodeCoeffs[TermState, Term, Double, shapeless.::[Typ[Term], shapeless.HNil], Term]] = Some(
  BaseCons(
    BasePi(provingground.learning.RandomVarFamily$$Lambda$3554/221246939@25eb7b07, TermsWithTyp),
    0.16500000000000004,
    BaseCons(
      BasePi(provingground.learning.GeneratorNode$$Lambda$3557/663473340@3320e553, TermsWithTyp),
      0.1,
      BaseCons(
        BasePi(provingground.learning.GeneratorNode$$Lambda$3557/663473340@4a372e85, TermsWithTyp),
        0.1,
        BaseCons(
          BasePi(provingground.learning.GeneratorNode$$Lambda$3557/663473340@522883d5, TermsWithTyp),
          0.1,
          BaseCons(
            BasePiOpt(
              provingground.learning.TermGeneratorNodes$$Lambda$3547/887487836@25367d65,
              TermsWithTyp
            ),
            0.485,
            Target(TermsWithTyp)
          )
        )
      )
    )
  )
)

















In [13]:



    


coeffs.map(_.rv)



    


















    
Out[13]:








res12: Vector[RandomVar[Any]] = Vector(
  Terms,
  AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil)
)

















In [14]:



    


coeffs.map(_.node)



    


















    
Out[14]:








res13: Vector[GeneratorNode[Any]] = Vector(
  ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms),
  Island(
    AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil),
    PiOutput(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }),
    AddVar(𝒰 , 0.3),
    Lambda,
    InIsle
  )
)

















In [15]:



    


val eqgs = Equation.group(eqs)



    


















    
Out[15]:








eqgs: Set[Equation] = Set(
  Equation(
    InitialVal(
      InIsle(
        InIsle(Elem(𝒰 , Typs), @b, Island(Typs, ConstRandVar(Typs), AddVar(𝒰 , 0.3), Sigma, InIsle)),
        @a,
        Island(Typs, ConstRandVar(Typs), AddVar(𝒰 , 0.3), Pi, InIsle)
      )
    ),
    Product(
      IsleScale(@b, Elem(𝒰 , Typs)),
      InitialVal(InIsle(Elem(𝒰 , Typs), @a, Island(Typs, ConstRandVar(Typs), AddVar(𝒰 , 0.3), Pi, InIsle)))
    )
  ),
  Equation(
    FinalVal(
      InIsle(
        InIsle(Elem(@a, Typs), @b, Island(Typs, ConstRandVar(Typs), AddVar(𝒰 , 0.3), Pi, InIsle)),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
      )
    ),
    Product(
      Coeff(Init(Typs), Typs),
      InitialVal(
        InIsle(
          InIsle(Elem(@a, Typs), @b, Island(Typs, ConstRandVar(Typs), AddVar(𝒰 , 0.3), Pi, InIsle)),
          @a,
          Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
        )
      )
    )
  ),
  Equation(
    InitialVal(InIsle(Elem(𝒰 , Typs), @a, Island(Typs, ConstRandVar(Typs), AddVar(𝒰 , 0.3), Pi, InIsle))),
    Product(IsleScale(@a, Elem(𝒰 , Typs)), InitialVal(Elem(𝒰 , Typs)))
  ),
  Equation(
    FinalVal(Elem(Wrap((@a : 𝒰 ) ↦ (_ : @a) ↦ 𝒰 ), AtCoord(FuncsWithDomain, 𝒰  :: HNil))),
    Product(
      Coeff(
        Island(AtCoord(FuncsWithDomain, 𝒰  :: HNil), ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle),
        AtCoord(FuncsWithDomain, 𝒰  :: HNil)
      ),
      FinalVal(
        InIsle(
          Elem((_ : @a) ↦ 𝒰 , Terms),
          @a,
          Island(
...

















In [16]:



    


val atoms = eqs.map(_.rhs).flatMap(Expression.atoms)



    


















    
Out[16]:








atoms: Set[Expression] = Set(
  FinalVal(InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))),
  InitialVal(
    InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
  ),
  IsleScale(@b, Elem(@b, Typs)),
  IsleScale(@a, Elem(@a, Terms)),
  InitialVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ),
  FinalVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ),
  InitialVal(Elem(@a, Terms)),
  FinalVal(
    InIsle(
      Elem(∏(@b : 𝒰 ){ @b }, Typs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ),
  FinalVal(Elem(((__1 , __2) : 𝒰 ×(𝒰  → 𝒰 )) ↦ 𝒰 , Terms)),
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Terms),
            @a,
            Island(
              AtCoord(TermsWithTyp, ((@a → @b) → @b) :: HNil),
              ConstRandVar(AtCoord(TermsWithTyp, @b :: HNil)),
              AddVar((@a → @b), 0.3),
              Lambda,
              InIsle
            )
          ),
          @a,
          Island(
            AtCoord(TermsWithTyp, (@a → ((@a → @b) → @b)) :: HNil),
...

















In [17]:



    


import ExpressionEval._



    


















    
Out[17]:








import ExpressionEval._

















In [18]:



    


val init = initMap(atoms, tg, ts)



    


















    
Out[18]:








init: Map[Expression, Double] = Map(
  IsleScale(@b, Elem(@b, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  Coeff(
    Map(
      provingground.learning.TermRandomVars$TargetTyps$$$Lambda$3560/1853403043@4a496499,
      Goals,
      TargetTyps
    ),
    TargetTyps
  ) -> 0.7,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  IsleScale(@a, Elem(𝒰 , Terms)) -> 0.7,
  Coeff(
    Island(
      AtCoord(TermsWithTyp, ((@a → @b) → @b) :: HNil),
      ConstRandVar(AtCoord(TermsWithTyp, @b :: HNil)),
      AddVar((@a → @b), 0.3),
      Lambda,
      InIsle
    ),
    AtCoord(TermsWithTyp, ((@a → @b) → @b) :: HNil)
  ) -> 0.485,
  InitialVal(Elem((@a_1 , @a_2), Terms)) -> 0.4285714285714286,
  IsleScale(@a, Elem(@a, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, AtCoord(TermsWithTyp, 𝒰  :: HNil))) -> 0.7,
  IsleScale(@a, Elem(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, Goals)) -> 0.7,
  IsleScale((@a_1 , @a_2), Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(∏(B : 𝒰 ){ (@a → ((@a → B) → B)) }, Goals)) -> 0.7,
  Coeff(
    Island(
      AtCoord(TermsWithTyp, (𝒰  → 𝒰 ) :: HNil),
      ConstRandVar(AtCoord(TermsWithTyp, 𝒰  :: HNil)),
      AddVar(𝒰 , 0.3),
      Lambda,
      InIsle
    ),
    AtCoord(TermsWithTyp, (𝒰  → 𝒰 ) :: HNil)
  ) -> 0.485,
...

















In [19]:



    


init.size



    


















    
Out[19]:








res18: Int = 176

















In [20]:



    


val m2 = nextMap(init, eqgs)



    


















    
Out[20]:








m2: Map[Expression, Double] = Map(
  InitialVal(
    InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
  ) -> 0.7,
  IsleScale(@b, Elem(@b, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  InitialVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.7,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  Coeff(
    Map(
      provingground.learning.TermRandomVars$TargetTyps$$$Lambda$3560/1853403043@4a496499,
      Goals,
      TargetTyps
    ),
    TargetTyps
  ) -> 0.7,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  IsleScale(@a, Elem(𝒰 , Terms)) -> 0.7,
  Coeff(
    Island(
      AtCoord(TermsWithTyp, ((@a → @b) → @b) :: HNil),
      ConstRandVar(AtCoord(TermsWithTyp, @b :: HNil)),
      AddVar((@a → @b), 0.3),
      Lambda,
      InIsle
    ),
    AtCoord(TermsWithTyp, ((@a → @b) → @b) :: HNil)
  ) -> 0.485,
  InitialVal(Elem((@a_1 , @a_2), Terms)) -> 0.4285714285714286,
  InitialVal(
    InIsle(
      Elem(∏(B : 𝒰 ){ (@a → ((@a → B) → B)) }, Goals),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
...

















In [21]:



    


m2.size



    


















    
Out[21]:








res20: Int = 282

















In [22]:



    


val m3 = nextMap(m2, eqgs)



    


















    
Out[22]:








m3: Map[Expression, Double] = Map(
  FinalVal(InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))) -> 0.42,
  InitialVal(
    InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
  ) -> 0.7,
  IsleScale(@b, Elem(@b, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  InitialVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.7,
  FinalVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.42,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  Coeff(
    Map(
      provingground.learning.TermRandomVars$TargetTyps$$$Lambda$3560/1853403043@4a496499,
      Goals,
      TargetTyps
    ),
    TargetTyps
  ) -> 0.7,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  InitialVal(
    InIsle(
      InIsle(Elem(@a, Terms), @a, Island(Terms, ConstRandVar(Terms), AddVar(@a, 0.3), Lambda, InIsle)),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.21,
  IsleScale(@a, Elem(𝒰 , Terms)) -> 0.7,
  Coeff(
...

















In [23]:



    


m3.size



    


















    
Out[23]:








res22: Int = 437

















In [24]:



    


eqgs.map(_.lhs).toSet -- m3.keySet



    


















    
Out[24]:








res23: Set[Expression] = Set(
  FinalVal(
    InIsle(
      InIsle(
        Elem((@a → ((@a → @b) → @b)), TargetTyps),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ),
  FinalVal(
    InIsle(
      Elem(∏(@b : 𝒰 ){ @b }, Typs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ),
  FinalVal(Elem(((__1 , __2) : 𝒰 ×(𝒰  → 𝒰 )) ↦ 𝒰 , Terms)),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Terms),
            @a,
            Island(
              AtCoord(TermsWithTyp, ((@a → @b) → @b) :: HNil),
              ConstRandVar(AtCoord(TermsWithTyp, @b :: HNil)),
              AddVar((@a → @b), 0.3),
              Lambda,
              InIsle
            )
          ),
          @a,
          Island(
            AtCoord(TermsWithTyp, (@a → ((@a → @b) → @b)) :: HNil),
            ConstRandVar(AtCoord(TermsWithTyp, ((@a → @b) → @b) :: HNil)),
            AddVar(@a, 0.3),
            Lambda,
            InIsle
          )
        ),
        @b,
        Island(
          AtCoord(TermsWithTyp, ∏(B : 𝒰 ){ (@a → ((@a → B) → B)) } :: HNil),
          PiOutput(∏(B : 𝒰 ){ (@a → ((@a → B) → B)) }),
          AddVar(𝒰 , 0.3),
...

















In [25]:



    


val zeroFirst = eqs.map(_.rhs).filter(exp => recExp(init, exp) == 0)



    


















    
Out[25]:








zeroFirst: Set[Expression] = Set(
  Product(
    Coeff(
      FlatMap(Typs, provingground.learning.TermGeneratorNodes$$Lambda$3549/1725945319@607b497, Typs),
      Typs
    ),
    FinalVal(
      InIsle(
        InIsle(Elem(𝒰 , Typs), @a, Island(Typs, ConstRandVar(Typs), AddVar(@a, 0.3), Pi, InIsle)),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
      )
    )
  ),
  Product(
    IsleScale(@a, Elem(@a, Terms)),
    InitialVal(
      InIsle(
        InIsle(
          InIsle(
            Elem(@a, Terms),
            @a,
            Island(
              AtCoord(TermsWithTyp, (@a → ((@a → @b) → @b)) :: HNil),
              ConstRandVar(AtCoord(TermsWithTyp, ((@a → @b) → @b) :: HNil)),
              AddVar(@a, 0.3),
              Lambda,
              InIsle
            )
          ),
          @b,
          Island(
            AtCoord(TermsWithTyp, ∏(B : 𝒰 ){ (@a → ((@a → B) → B)) } :: HNil),
            PiOutput(∏(B : 𝒰 ){ (@a → ((@a → B) → B)) }),
            AddVar(𝒰 , 0.3),
            Lambda,
            InIsle
          )
        ),
        @a,
        Island(
          AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil),
          PiOutput(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }),
          AddVar(𝒰 , 0.3),
          Lambda,
          InIsle
        )
      )
...

















In [26]:



    


zeroFirst.size



    


















    
Out[26]:








res25: Int = 587

















In [27]:



    


val step2 = zeroFirst.filter(exp => recExp(m2, exp) != 0)



    


















    
Out[27]:








step2: Set[Expression] = Set(
  Product(
    IsleScale(@b, Elem(@a, Typs)),
    InitialVal(
      InIsle(Elem(@a, Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
    )
  ),
  Product(
    IsleScale(@a, Elem(@a, Typs)),
    InitialVal(InIsle(Elem(@a, Typs), @a, Island(Typs, ConstRandVar(Typs), AddVar(𝒰 , 0.3), Pi, InIsle)))
  ),
  Product(
    Coeff(Init(Typs), Typs),
    InitialVal(
      InIsle(
        Elem(𝒰 , Typs),
        (@a_1 , @a_2),
        Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
      )
    )
  ),
  Product(
    Coeff(Init(Terms), Terms),
    InitialVal(
      InIsle(
        Elem(𝒰 , Terms),
        @a,
        Island(
          AtCoord(TermsWithTyp, ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } } :: HNil),
          PiOutput(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }),
          AddVar(𝒰 , 0.3),
          Lambda,
          InIsle
        )
      )
    )
  ),
  Product(
    Coeff(Init(Terms), Terms),
    InitialVal(
      InIsle(
        Elem((@a_1 , @a_2), Terms),
        (@a_1 , @a_2),
        Island(Terms, ConstRandVar(Terms), AddVar(∏(@a : 𝒰 ){ @a }×𝒰 , 0.3), Lambda, InIsle)
      )
    )
  ),
  Product(
    IsleScale(@a, Elem(@a, Terms)),
...

















In [28]:



    


step2.size



    


















    
Out[28]:








res27: Int = 141

















In [29]:



    


m2.filter(_._2 == 0).size
m3.filter(_._2 == 0).size



    


















    
Out[29]:








res28_0: Int = 0
res28_1: Int = 0

















In [30]:



    


val ms = stableSupportMap(init, eqgs)



    


















    
Out[30]:








ms: Map[Expression, Double] = Map(
  FinalVal(InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))) -> 0.42,
  InitialVal(
    InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
  ) -> 0.7,
  IsleScale(@b, Elem(@b, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  FinalVal(
    InIsle(
      InIsle(
        Elem((@a → ((@a → @b) → @b)), TargetTyps),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.147,
  InitialVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.7,
  FinalVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.42,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  FinalVal(
    InIsle(
      Elem(∏(@b : 𝒰 ){ @b }, Typs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.013150807492591156,
  FinalVal(Elem(((__1 , __2) : 𝒰 ×(𝒰  → 𝒰 )) ↦ 𝒰 , Terms)) -> 0.0385060355554574,
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Terms),
            @a,
...

















In [31]:



    


m2.filter(_._2 == 0)



    


















    
Out[31]:








res30: Map[Expression, Double] = Map()

















In [32]:



    


m3.filter(_._2 == 0)



    


















    
Out[32]:








res31: Map[Expression, Double] = Map()

















In [33]:



    


val m4 = nextMap(m3, eqgs)



    


















    
Out[33]:








m4: Map[Expression, Double] = Map(
  FinalVal(InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))) -> 0.42,
  InitialVal(
    InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
  ) -> 0.7,
  IsleScale(@b, Elem(@b, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  InitialVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.7,
  FinalVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.42,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  FinalVal(Elem(((__1 , __2) : 𝒰 ×(𝒰  → 𝒰 )) ↦ 𝒰 , Terms)) -> 0.038500000000000006,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  Coeff(
    Map(
      provingground.learning.TermRandomVars$TargetTyps$$$Lambda$3560/1853403043@4a496499,
      Goals,
      TargetTyps
    ),
    TargetTyps
  ) -> 0.7,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  InitialVal(
    InIsle(
      InIsle(Elem(@a, Terms), @a, Island(Terms, ConstRandVar(Terms), AddVar(@a, 0.3), Lambda, InIsle)),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.21,
  FinalVal(
...

















In [34]:



    


val ms = stableSupportMap(init, eqgs)



    


















    
Out[34]:








ms: Map[Expression, Double] = Map(
  FinalVal(InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))) -> 0.42,
  InitialVal(
    InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
  ) -> 0.7,
  IsleScale(@b, Elem(@b, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  FinalVal(
    InIsle(
      InIsle(
        Elem((@a → ((@a → @b) → @b)), TargetTyps),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.147,
  InitialVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.7,
  FinalVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.42,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  FinalVal(
    InIsle(
      Elem(∏(@b : 𝒰 ){ @b }, Typs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.013150807492591156,
  FinalVal(Elem(((__1 , __2) : 𝒰 ×(𝒰  → 𝒰 )) ↦ 𝒰 , Terms)) -> 0.0385060355554574,
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Terms),
            @a,
...

















In [35]:



    


val mss = nextMap(ms, eqgs)



    


















    
Out[35]:








mss: Map[Expression, Double] = Map(
  FinalVal(InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))) -> 0.42,
  InitialVal(
    InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
  ) -> 0.7,
  IsleScale(@b, Elem(@b, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  FinalVal(
    InIsle(
      InIsle(
        Elem((@a → ((@a → @b) → @b)), TargetTyps),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.147,
  InitialVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.7,
  FinalVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.42,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  FinalVal(
    InIsle(
      Elem(∏(@b : 𝒰 ){ @b }, Typs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.013151570681494687,
  FinalVal(Elem(((__1 , __2) : 𝒰 ×(𝒰  → 𝒰 )) ↦ 𝒰 , Terms)) -> 0.03850605967906028,
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Terms),
            @a,
...

















In [36]:



    


mapRatio(ms, mss)



    


















    
Out[36]:








res35: Double = 3.1003174836561977

















In [37]:



    


val m100 = iterateMap(ms, eqgs, 100)



    


















    
Out[37]:








m100: Map[Expression, Double] = Map(
  FinalVal(InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))) -> 0.42,
  InitialVal(
    InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
  ) -> 0.7,
  IsleScale(@b, Elem(@b, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  FinalVal(
    InIsle(
      InIsle(
        Elem((@a → ((@a → @b) → @b)), TargetTyps),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.147,
  InitialVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.7,
  FinalVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.42,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  FinalVal(
    InIsle(
      Elem(∏(@b : 𝒰 ){ @b }, Typs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.013152400835073068,
  FinalVal(Elem(((__1 , __2) : 𝒰 ×(𝒰  → 𝒰 )) ↦ 𝒰 , Terms)) -> 0.03850609129352404,
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Terms),
            @a,
...

















In [38]:



    


val m200 = iterateMap(m100, eqgs, 100)



    


















    
Out[38]:








m200: Map[Expression, Double] = Map(
  FinalVal(InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))) -> 0.42,
  InitialVal(
    InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
  ) -> 0.7,
  IsleScale(@b, Elem(@b, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  FinalVal(
    InIsle(
      InIsle(
        Elem((@a → ((@a → @b) → @b)), TargetTyps),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.147,
  InitialVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.7,
  FinalVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.42,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  FinalVal(
    InIsle(
      Elem(∏(@b : 𝒰 ){ @b }, Typs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.013152400835073068,
  FinalVal(Elem(((__1 , __2) : 𝒰 ×(𝒰  → 𝒰 )) ↦ 𝒰 , Terms)) -> 0.03850609129352404,
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Terms),
            @a,
...

















In [39]:



    


mapRatio(m100, m200)



    


















    
Out[39]:








res38: Double = 1.0000000000000013

















In [40]:



    


val m201 = nextMap(m200, eqgs)



    


















    
Out[40]:








m201: Map[Expression, Double] = Map(
  FinalVal(InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))) -> 0.42,
  InitialVal(
    InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
  ) -> 0.7,
  IsleScale(@b, Elem(@b, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  FinalVal(
    InIsle(
      InIsle(
        Elem((@a → ((@a → @b) → @b)), TargetTyps),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.147,
  InitialVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.7,
  FinalVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.42,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  FinalVal(
    InIsle(
      Elem(∏(@b : 𝒰 ){ @b }, Typs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.013152400835073068,
  FinalVal(Elem(((__1 , __2) : 𝒰 ×(𝒰  → 𝒰 )) ↦ 𝒰 , Terms)) -> 0.03850609129352404,
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Terms),
            @a,
...

















In [46]:



    


stableMap(init, eqgs)



    


















    
Out[46]:








res45: Map[Expression, Double] = Map(
  FinalVal(InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))) -> 0.42,
  InitialVal(
    InIsle(Elem(𝒰 , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle))
  ) -> 0.7,
  IsleScale(@b, Elem(@b, Typs)) -> 0.7,
  IsleScale(@a, Elem(@a, Terms)) -> 0.7,
  FinalVal(
    InIsle(
      InIsle(
        Elem((@a → ((@a → @b) → @b)), TargetTyps),
        @b,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
      ),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.147,
  InitialVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.7,
  FinalVal(
    InIsle(
      Elem(𝒰 , Typs),
      (@a_1 , @a_2),
      Island(Typs, ConstRandVar(Typs), AddVar(∑(@a : { @a }, 0.3), Pi, InIsle)
    )
  ) -> 0.42,
  InitialVal(Elem(@a, Terms)) -> 0.4285714285714286,
  FinalVal(
    InIsle(
      Elem(∏(@b : 𝒰 ){ @b }, Typs),
      @a,
      Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, InIsle)
    )
  ) -> 0.013152400788112117,
  FinalVal(Elem(((__1 , __2) : 𝒰 ×(𝒰  → 𝒰 )) ↦ 𝒰 , Terms)) -> 0.03850609128852615,
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Terms),
            @a,
...

















In [ ]:



    






    











In [ ]:



    






    











In [ ]:

Content source: siddhartha-gadgil/ProvingGround

Similar notebooks:

notebook.community | gallery | about