Derived equations

We illustrate in a simple case deriving equations to generate a term. This is useful if terms and types have come externally, for instance by experimentation or from the literature.

import $cp.bin.`provingground-core-jvm-e0f46c1def.fat.jar`

import $cp.$                                              

import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}

import provingground._ , interface._, HoTT._, learning._ 

First we define some terms and types

val A = Type.sym
val B = Type.sym
val a = A.sym
val f = "f" :: A ->: B
val mp = a :-> (f :-> f(a))

A: Typ[Term] = A
B: Typ[Term] = B
a: Term = a
f: Func[Term, Term] = f
mp: Func[Term, Func[Func[Term, Term], Term]] = (a : A) ↦ (f : (A → B)) ↦ f(a)

We derive equations and construct an expression evaluator

val de = new DerivedEquations

val tg = TermGenParams()
val ts = TermState(FiniteDistribution(), FiniteDistribution.unif(A, B))
val eqNodes = de.formalEquations(mp) union de.termStateInit(ts)

val ev = ExpressionEval.fromInitEqs(ts, Equation.group(eqNodes), tg)

de: DerivedEquations = provingground.learning.DerivedEquations@17068831
tg: TermGenParams = 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
)
ts: TermState = TermState(
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
eqNodes: Set[EquationNode] = Set(
  EquationNode(
    FinalVal(
      InIsle(
        Elem(a, Terms),
        a,
        Island(Terms, ConstRandVar(Terms), AddVar(A, 0.3), Lambda, EnterIsle)
      )
    ),
    Product(
      Coeff(Init(Terms)),
      InitialVal(
        InIsle(
          Elem(a, Terms),
          a,
          Island(Terms, ConstRandVar(Terms), AddVar(A, 0.3), Lambda, EnterIsle)
        )
      )
    )
  ),
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(Wrap(f), Funcs),
          f,
          Island(
            Terms,
            ConstRandVar(Terms),
            AddVar((A → B), 0.3),
            Lambda,
            EnterIsle
          )
        ),
        a,
        Island(Terms, ConstRandVar(Terms), AddVar(A, 0.3), Lambda, EnterIsle)
      )
    ),
    Product(
...
ev: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@721d9277

We check that we can generate mp

ev.finalTerms

res4: FiniteDistribution[Term] = FiniteDistribution(
  Vector(Weighted((a : A) ↦ (f : (A → B)) ↦ f(a), 0.5), Weighted(A, 0.5))
)

First conclusion: We successfully generated modus ponens depending on $A$ and $B$.

We next turn to Modus Ponens, but in its full (universal) form

val mpU = A :~> (B :~> mp)
val tsU = TermState(FiniteDistribution(), FiniteDistribution.unif(Type))
val eqNodesU = de.formalEquations(mpU) union de.termStateInit(tsU)
val evU = ExpressionEval.fromInitEqs(tsU, Equation.group(eqNodesU), tg)
evU.finalTerms

mpU: FuncLike[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]] = (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (f : (A → B)) ↦ f(a)
tsU: TermState = TermState(
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
eqNodesU: Set[EquationNode] = Set(
  EquationNode(
    InitialVal(
      InIsle(
        InIsle(
          Elem(𝒰 , Terms),
          B,
          Island(
            Terms,
            ConstRandVar(Terms),
            AddVar(𝒰 , 0.3),
            Lambda,
            EnterIsle
          )
        ),
        A,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, EnterIsle)
      )
    ),
    Product(
      IsleScale(B, Elem(𝒰 , Terms)),
      FinalVal(
        InIsle(
          Elem(𝒰 , Terms),
          A,
          Island(
            Terms,
            ConstRandVar(Terms),
            AddVar(𝒰 , 0.3),
            Lambda,
            EnterIsle
          )
        )
      )
    )
  ),
  EquationNode(
    InitialVal(
      InIsle(
...
evU: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@3f95f2d3
res5_4: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(𝒰 , 0.5),
    Weighted((A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (f : (A → B)) ↦ f(a), 0.5)
  )
)

Conclusion

We see that derived equations allow us to generate Modus Ponens.