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 [ ]: