implication.kt

package com.fnreport.symbolic

//Table B.8. The implication theorems.
//statement1 ⇒ statement2

//f1,f2,  the unicode infix
typealias  F = (Term, Term) -> Statement

//confidence value p 51
typealias  C = Float

interface Statement : Term {
    val z: List<Pair<Term, Pair<F?, C?>?>>
}

interface Term

operator fun Term.invoke(): Boolean {
    TODO()
}

operator fun Term.invoke(t: Term): Statement {
    TODO()
}

//bag relation op.
operator fun Term.inc(): Term = TODO()

operator fun Statement.component1(): Term = z.let { (x) -> x.let { (term) -> term } }
operator fun Statement.component2(): Term = z.let { (_, x) -> x.let { (term) -> term } }
operator fun Statement.component3(): Term = z.let { (_, _, x) -> x.let { (term: Term) -> term } }
operator fun Statement.component4(): Term = z.let { (_, _, _, x) -> x.let { (term: Term) -> term } }
interface Qry : Term

/**
 * J1 is "between" P and M.
 */

operator fun Term.rangeTo(m: Term): Iterable<Term> {
    TODO("not implemented") //To change body of created functions use File | Settings | File Templates.
}

//val `↔`: F = TODO()

infix fun Term.`↔`(t: Term): Statement {
    TODO()
}

infix fun Term.`→`(t: Term): Statement {
    TODO()
}

infix fun Term.`⇒`(t: Term): Statement {
    TODO()
}

infix fun Term.`⇔`(t: Term): Statement {
    TODO()
}

infix fun Term.`∧`(t: Term): Statement {
    TODO()
}

infix fun Term.`∨`(t: Term): Statement {
    TODO()
}

infix fun Term.`∪`(t: Term): Statement {
    TODO()
}

infix fun Term.`∩`(t: Term): Statement {
    TODO()
}

infix fun Term.`−`(t: Term): Statement {
    TODO()
}

infix fun Term.`⦵`(t: Term): Statement {
    TODO()
}

infix fun Term.`¬`(t: Term): Statement {
    TODO()
}

infix fun Term.`╱`(t: Term): Statement {
    TODO()
}

infix fun Term.`╲`(t: Term): Statement {
    TODO()
}

//Table B.1. The first-order syllogistic rules.
//J2\J1 M → P f1, c1 P → M f1, c1 M ↔ P f1, c1
//S → P Fded S → P Fabd S → P F

//ana
//S → M f2, c2 P → S F

//exe P → S F

//abd
//S ↔ P F

//com
//S → P Find S → P Fexe
//M → S f2, c2 P → S F

//ind P → S F

//ded P → S F

//ana
//S ↔ P Fcom
//S → P Fana
//S ↔ M f2, c2 P → S Fana
//S ↔ P Fres


fun Statement.normalize(J: Array<Term>, T: Array<Qry>): Any {
    var (P, S, M, _) = z.map { (t: Term) -> t }
    val (T1, T2) = T

    val (J1, J2) = J

    val (S1, S2) = listOf<Term>(S, S++)

//Table B.2. The conditional syllogistic rules.
//J1 f1, c1 J2 f2, c2 J F
//aassertions?
//    S S ⇔ P PFana   TODO()?
//    S PS ⇔ P Fcom   TODO()?
//    S ⇒ P S PFded   TODO()?
//    P ⇒ S S PFabd   TODO()?
//    P SS ⇒ P Find   TODO()?
//    (C ∧ S) ⇒ P SC ⇒ P Fded
//    (C ∧ S) ⇒ P C ⇒ P SFabd
//    C ⇒ P S (C ∧ S) ⇒ P Find
//    (C ∧ S) ⇒ P M ⇒ S (C ∧ M) ⇒ P Fded
//    (C ∧ S) ⇒ P (C ∧ M) ⇒ P M ⇒ S Fabd
//    (C ∧ M) ⇒ P M ⇒ S (C ∧ S) ⇒ P Find


//    implication//
    /**
     * p 51.  M is shared term
     */
    return if (J1 in (P..M) && (J2 in S..M))
        when (S) {
            S `↔` P -> S `→` P
            S `⇔` P -> S `⇒` P
            S1 `∧` S2 -> S1
            S1 -> S1 `∨` S2
            S `→` P -> (S `∪` M) `→` (P `∪` M)
            S `→` P -> (S `∩` M) `→` (P `∩` M)
            S `↔` P -> (S `∪` M) `↔` (P `∪` M)
            S `↔` P -> (S `∩` M) `↔` (P `∩` M)
            S `⇒` P -> (S `∨` M) `⇒` (P `∨` M)
            S `⇒` P -> (S `∧` M) `⇒` (P `∧` M)
            S `⇔` P -> (S `∨` M) `⇔` (P `∨` M)
            S `⇔` P -> (S `∧` M) `⇔` (P `∧` M)
            S `→` P -> (S `−` M) `→` (P `−` M)
            S `→` P -> (M `−` P) `→` (M `−` S)
            S `→` P -> (S `⦵` M) `→` (P `⦵` M)
            S `→` P -> (M `⦵` P) `→` (M `⦵` S)
            S `↔` P -> (S `−` M) `↔` (P `−` M)
            S `↔` P -> (M `−` P) `↔` (M `−` S)
            S `↔` P -> (S `⦵` M) `↔` (P `⦵` M)
            S `↔` P -> (M `⦵` P) `↔` (M `⦵` S)
            M `→` (T1 `−` T2) -> `¬`(M `→` T2)
            (T1 `⦵` T2) `→` M -> `¬`(T2 `→` M)
            S `→` P -> (S `╱` M) `→` (P `╱` M)
            S `→` P -> (S `╲` M) `→` (P `╲` M)
            S `→` P -> (M `╱` P) `→` (M `╱` S)
            S `→` P -> (M `╲` P) `→` (M `╲` S)
        }
}


fun Statement.composition(J: Array<Term>, T: Array<Qry>): Any {

    var (P, S, M, _) = z.map { (t: Term) -> t }
    val (T1, T2) = T

    val (J1, J2) = J

    val (S1, S2) = listOf<Term>(S, S++)


//    Table B.3. The composition rules.
//            J1 f1, c1 J2 f2, c2 J F

    when {
        (M `→` T1)() &&/* and */ (M `→` T2)() -> {
            M `→` (T1 `∩` T2) //Fint TODO() //reassign F above?
            M `→` (T1 `∪` T2) //Funi TODO() //reassign F above?
            M `→` (T1 `−` T2) //Fdif TODO() //reassign F above?
            M `→` (T2 `−` T1) //F
dif TODO() //reassign F above?
        }
        when ((T1 `→` M)() && (T2 `→` M)()) {
            true -> {
                (T1 ∪ T2) → M) //  Fint
                (T1 `∩` T2) `→` M //Funi
                (T1 `⦵` T2) `→` M //Fdif
                (T2 `⦵` T1) `→` M //F
dif
            }
        }
            when((M `⇒` T1)   (M `⇒` T2)()){
            true->
            M `⇒` (T1 `∧` T2) //Fint
            M `⇒` (T1 ∨ T2) //Funi
        }
        when {
            ((T1 `⇒` M)() && (T2 `⇒` M)())
            -> {
                (T1 `∨` T2) `⇒` M //Fint
                (T1 `∧` T2) `⇒` M //Funi
            }
        }

            if (T1(T2))   {
            T1 `∧` T2 //Fint
            T1 `∨` T2
        } //Funi


}}

/**
Table B.4. The decomposition rules.
S1 S2 S
¬(M → (T1 ∩ T2)) M → T1 ¬(M → T2)
M → (T1 ∪ T2) ¬(M → T1) M → T2
¬(M → (T1 − T2)) M → T1 M → T2
¬(M → (T2 − T1)) ¬(M → T1) ¬(M → T2)
¬((T1 ∪ T2) → M) T1 → M ¬(T2 → M)
(T1 ∩ T2) → M ¬(T1 → M) T2 → M
¬((T1
T2) → M) T1 → M T2 → M
¬((T2
T1) → M) ¬(T1 → M) ¬(T2 → M)
¬(T1 ∧ T2) T1 ¬T2
T1 ∨ T2 ¬T1 T2
 */
fun Statement.composition(J: Array<Term>, T: Array<Qry>): Any {

    var (P, S, M, _) = z.map { (t: Term) -> t }
    val (T1, T2) = T

    val (J1, J2) = J

    val (S1, S2) = listOf<Term>(S, S++)
when (S){ 
//Table B.4. The decomposition rules.
//S1 S2 S

    `¬`(M `→` (T1 `∩` T2)) M `→` T1 `¬`(M `→` T2)`
`M `→` (T1 `∪` T2) `¬`(M `→` T1) M `→` T2`
¬`(M `→` (T1 `−` T2)) M `→` T1 M `→` T2`
¬`(M `→` (T2 `−` T1)) `¬`(M `→` T1) `¬`(M `→` T2)`
¬`((T1 `∪` T2) `→` M) T1 `→` M `¬`(T2 `→` M)`
`(T1 `∩` T2) `→` M `¬`(T1 `→` M) T2 `→` M`
¬`((T1`
`T2) `→` M) T1 `→` M T2 `→` M`
¬`((T2`
`T1) `→` M) `¬`(T1 `→` M) `¬`(T2 `→` M)`
¬`(T1 `∧` T2) T1 `¬`T2`
`T1 `∨` T2 `¬`T1 T2