Modus Ponens: statement, proof from goal, formal equations¶

we repeat the previous search for the statement of modus ponens
we then add this as a goal and look for a proof
given the proof, we look for formal equations and add these to the expression eval
finally check whether with these equations but without the goal, we get a proof of modus ponens. If not, figure out what fails.

import $cp.bin.`provingground-core-jvm-b8c7356944.fat.jar`
import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}

import $cp.$                                              

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

val A = "A" :: Type
val B = "B" :: Type

val ts = TermState(FiniteDistribution.unif(A, B), FiniteDistribution.unif(A, B, Type), vars = Vector(A, B))

val MPAB = A ->: (A ->: B) ->: B
val MP = A ~>: (B ~>: MPAB)

A: Typ[Term] = A
B: Typ[Term] = B
ts: TermState = TermState(
  FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
  FiniteDistribution(
    Vector(
      Weighted(A, 0.3333333333333333),
      Weighted(B, 0.3333333333333333),
      Weighted(𝒰 , 0.3333333333333333)
    )
  ),
  Vector(A, B),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
MPAB: FuncTyp[Term, Func[Func[Term, Term], Term]] = (A → ((A → B) → B))
MP: GenFuncTyp[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]] = ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }

val lp1 = LocalProver(ts, tg = TermGenParams(sigmaW = 0), relativeEval = true).sharpen(10)

lp1: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(Vector(Weighted(A, 0.5), Weighted(B, 0.5))),
    FiniteDistribution(
      Vector(
        Weighted(A, 0.3333333333333333),
        Weighted(B, 0.3333333333333333),
        Weighted(𝒰 , 0.3333333333333333)
      )
    ),
    Vector(A, B),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
    0.1,
    0.1,
    0.1,
    0.05,
    0.05,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.0,
    0.0
  ),
  1.0E-5,
  12 minutes,
  1.01,
  1.0,
...

import monix.execution.Scheduler.Implicits.global
val evT1 = lp1.expressionEval
evT1.map(_.finalTyps(MP)).runToFuture

import monix.execution.Scheduler.Implicits.global

evT1: monix.eval.Task[ExpressionEval] = Async(<function2>, false, true, true)
res3_2: monix.execution.CancelableFuture[Double] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(7.173348108620456E-4)

evT1.map(_.finalTerms.filter(_.typ == MP)).runToFuture

res4: monix.execution.CancelableFuture[FiniteDistribution[Term]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(FiniteDistribution(Vector()))

val ts2 = TermState(FiniteDistribution(), FiniteDistribution.unif(Type), goals = FiniteDistribution.unif(MP))

ts2: TermState = TermState(
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(Weighted(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, 1.0))
  ),
  Empty
)

val lp2 = LocalProver(ts2, tg = TermGenParams(sigmaW = 0), relativeEval = true).sharpen(10)

lp2: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(Weighted(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, 1.0))
    ),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
    0.1,
    0.1,
    0.1,
    0.05,
    0.05,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.0,
    0.0
  ),
  1.0E-5,
  12 minutes,
  1.01,
  1.0,
  10000,
  10,
  1.0,
  1.0,
...

val evT2 = lp2.expressionEval
evT2.map(_.finalTerms.filter(_.typ == MP)).runToFuture

evT2: monix.eval.Task[ExpressionEval] = Async(<function2>, false, true, true)
res7_1: monix.execution.CancelableFuture[FiniteDistribution[Term]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  FiniteDistribution(
    Vector(
      Weighted(
        (@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
        5.060827243615959E-4
      )
    )
  )
)

val mpPfsT = evT2.map(_.finalTerms.filter(_.typ == MP))
val mpEqsT = mpPfsT.map{pfs => pfs.support.flatMap(pf => DE.formalEquations(pf))}

mpPfsT: monix.eval.Task[FiniteDistribution[Term]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd8$Helper$$Lambda$2839/620242560@232667c,
  0
)
mpEqsT: monix.eval.Task[Set[EquationNode]] = Map(
  Async(<function2>, false, true, true),
  scala.Function1$$Lambda$296/951031848@4aa1db02,
  1
)

mpEqsT.runToFuture

res9: monix.execution.CancelableFuture[Set[EquationNode]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  Set(
    EquationNode(
      InitialVal(
        InIsle(
          Elem(𝒰 , Terms),
          @a,
          Island(
            Terms,
            ConstRandVar(Terms),
            AddVar(𝒰 , 0.3),
            Lambda,
            EnterIsle
          )
        )
      ),
      Product(IsleScale(@a, Elem(𝒰 , Terms)), FinalVal(Elem(𝒰 , Terms)))
    ),
    EquationNode(
      InitialVal(
        InIsle(
          InIsle(
            InIsle(
              InIsle(
                Elem(@b, Terms),
                @a,
                Island(Typs, ConstRandVar(Typs), AddVar(@a, 0.3), Pi, EnterIsle)
              ),
              @a,
              Island(
                Terms,
                ConstRandVar(Terms),
                AddVar(@a, 0.3),
                Lambda,
                EnterIsle
              )
            ),
            @b,
            Island(
...

val evT3 = for{
    ev <- evT2
    ev1 <- evT1
    eqs <- mpEqsT
} yield ev.modify(equationsNew = ev1.equations union Equation.group(eqs union DE.termStateInit(ts)) )

evT3: monix.eval.Task[ExpressionEval] = FlatMap(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd13$Helper$$Lambda$3191/1502492031@41817c3c
)

evT3.map(_.finalTerms.filter(_.typ == MP)).runToFuture

res14: monix.execution.CancelableFuture[FiniteDistribution[Term]] = Success(FiniteDistribution(Vector()))

evT3.map(_.finalTyps(Type)).runToFuture

res15: monix.execution.CancelableFuture[Double] = Success(0.981077207477083)

import GeneratorVariables._, Expression._, TermRandomVars._
val targT = evT3.map(ev => ev.equations.collect{case eq @ Equation(FinalVal(Elem(t : Term, Terms)), _) if t.typ == MP => eq})

import GeneratorVariables._, Expression._, TermRandomVars._

targT: monix.eval.Task[Set[Equation]] = Map(
  FlatMap(
    Async(<function2>, false, true, true),
    ammonite.$sess.cmd13$Helper$$Lambda$3191/1502492031@41817c3c
  ),
  ammonite.$sess.cmd16$Helper$$Lambda$3636/659289373@7fefc395,
  0
)

targT.runToFuture

res18: monix.execution.CancelableFuture[Set[Equation]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  Set(
    Equation(
      FinalVal(
        Elem(
          (@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
          Terms
        )
      ),
      Sum(
        Product(
          Product(
            Coeff(FlatMap(Typs, LambdaIsle, Terms)),
            FinalVal(Elem(𝒰 , Typs))
          ),
          FinalVal(
            InIsle(
              Elem((@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a), Terms),
              @a,
              Island(
                Terms,
                ConstRandVar(Terms),
                AddVar(𝒰 , 0.3),
                Lambda,
                EnterIsle
              )
            )
          )
        ),
        Product(
          Coeff(Init(Terms)),
          InitialVal(
            Elem(
              (@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
              Terms
            )
          )
        )
      )
...

Conclusions¶

The search steps succeeded, as did generating equations for modus ponens.
However, we did not get modus ponens as a consequence of the equations we tried.
The equations we tried were ad hoc; we should have a clean way of removing goal equations but adding formal equations.

val tsU = TermState(FiniteDistribution(), FiniteDistribution.unif(Type))
val a = "a" :: A
val f = "f" :: (A ->: B)
val mp = a :-> (f :-> f(a))
val mpU = A :~> (B :~> mp)
val eqNodesU = DE.formalEquations(mpU) union DE.termStateInit(tsU)

tsU: TermState = TermState(
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
a: Term = a
f: Func[Term, Term] = f
mp: Func[Term, Func[Func[Term, Term], Term]] = (a : A) ↦ (f : (A → B)) ↦ f(a)
mpU: FuncLike[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]] = (A : 𝒰 ) ↦ (B : 𝒰 ) ↦ (a : A) ↦ (f : (A → B)) ↦ f(a)
eqNodesU: Set[EquationNode] = Set(
  EquationNode(
    InitialVal(
      InIsle(
        Elem(𝒰 , Terms),
        A,
        Island(Terms, ConstRandVar(Terms), AddVar(𝒰 , 0.3), Lambda, EnterIsle)
      )
    ),
    Product(IsleScale(A, Elem(𝒰 , Terms)), FinalVal(Elem(𝒰 , Terms)))
  ),
  EquationNode(
    FinalVal(
      InIsle(
        InIsle(
          InIsle(
            InIsle(
              Elem(A, Terms),
              f,
              Island(
                Terms,
                ConstRandVar(Terms),
                AddVar((A → B), 0.3),
                Lambda,
                EnterIsle
              )
            ),
            a,
            Island(
              Terms,
              ConstRandVar(Terms),
              AddVar(A, 0.3),
              Lambda,
              EnterIsle
            )
          ),
          B,
          Island(
            Terms,
...

val evU = ExpressionEval.fromInitEqs(tsU, Equation.group(eqNodesU), TermGenParams())

evU: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@f2bbab4

evU.finalTerms

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

evU.finalTerms(mpU)

res24: Double = 0.5

Conclusions round two¶

The above is self-contained (pasted from REPL) showing that we do get modus ponens if we work with equations. We should try this with equations for proofs as well.

val eqNodesUT = mpEqsT.map (_ union DE.termStateInit(tsU))

eqNodesUT: monix.eval.Task[Set[EquationNode]] = Map(
  Async(<function2>, false, true, true),
  scala.Function1$$Lambda$296/951031848@17165bea,
  2
)

val evUT = eqNodesUT.map{nodes => ExpressionEval.fromInitEqs(tsU, Equation.group(nodes) , TermGenParams())}

evUT: monix.eval.Task[ExpressionEval] = Map(
  Async(<function2>, false, true, true),
  scala.Function1$$Lambda$296/951031848@7b5764d9,
  3
)

evUT.map(_.finalTerms(mpU)).runToFuture

res27: monix.execution.CancelableFuture[Double] = Success(0.5)

evUT.map(_.finalTerms.filter(_.typ == MP)).runToFuture

res29: monix.execution.CancelableFuture[FiniteDistribution[Term]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  FiniteDistribution(
    Vector(
      Weighted(
        (@a : 𝒰 ) ↦ (@b : 𝒰 ) ↦ (@a : @a) ↦ (@a : (@a → @b)) ↦ @a(@a),
        0.5
      )
    )
  )
)

Final conclusions¶

When the equations are added correctly we do get proofs of modus ponens.
We should have more convenience methods