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.

In [1]:
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
    }
  )
}


Out[1]:
import $cp.$                                              

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

In [2]:
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)


Out[2]:
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)) } }

In [3]:
val lp1 = LocalProver(ts, tg = TermGenParams(sigmaW = 0), relativeEval = true).sharpen(10)


Out[3]:
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,
...

In [4]:
import monix.execution.Scheduler.Implicits.global
val evT1 = lp1.expressionEval
evT1.map(_.finalTyps(MP)).runToFuture



In [5]:
evT1.map(_.finalTerms.filter(_.typ == MP)).runToFuture



In [6]:
val ts2 = TermState(FiniteDistribution(), FiniteDistribution.unif(Type), goals = FiniteDistribution.unif(MP))


Out[6]:
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
)

In [7]:
val lp2 = LocalProver(ts2, tg = TermGenParams(sigmaW = 0), relativeEval = true).sharpen(10)


Out[7]:
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,
...

In [8]:
val evT2 = lp2.expressionEval
evT2.map(_.finalTerms.filter(_.typ == MP)).runToFuture



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


Out[9]:
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
)

In [10]:
mpEqsT.runToFuture



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


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

In [15]:
evT3.map(_.finalTerms.filter(_.typ == MP)).runToFuture



In [16]:
evT3.map(_.finalTyps(Type)).runToFuture



In [17]:
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})


Out[17]:
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
)

In [19]:
targT.runToFuture


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.

In [21]:
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)


Out[21]:
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,
...

In [22]:
val evU = ExpressionEval.fromInitEqs(tsU, Equation.group(eqNodesU), TermGenParams())


Out[22]:
evU: ExpressionEval = provingground.learning.ExpressionEval$$anon$2@f2bbab4

In [23]:
evU.finalTerms


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

In [25]:
evU.finalTerms(mpU)


Out[25]:
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.

In [26]:
val eqNodesUT = mpEqsT.map (_ union DE.termStateInit(tsU))


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

In [27]:
val evUT = eqNodesUT.map{nodes => ExpressionEval.fromInitEqs(tsU, Equation.group(nodes) , TermGenParams())}


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

In [28]:
evUT.map(_.finalTerms(mpU)).runToFuture



In [30]:
evUT.map(_.finalTerms.filter(_.typ == MP)).runToFuture


Final conclusions

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