

2015-06-02

output of the generalised delta-table algorithm on the proof generated by poset-experiment.scala:

Size of term set: 36

Number of grammars: 3
Smallest grammar-size: 32
Number of smallest grammars: 1

Minimized cut formula: ∀α_0.∀α_1.∀α_2.(α_0=f(α_0,α_2)∨¬α_0=α_0∨¬α_1=f(α_1,α_2)∨¬α_0=f(α_0,α_1)∨¬f(f(α_0,α_1),α_2)=f(α_0,α_2))
which is (almost) transitivity of the partial order x \leq y iff f(x,y)=x

grammars(0) (claimed to be minimal by generalised delta-table algorithm, size 32) is:

{
tuple1(a),
tuple1(b),
tuple1(c),
tuple2(b,a,f(b,c),a),
tuple2(c,b,f(c,a),b),
tuple2(α_0,α_1,α_0,f(α_1,α_2)),
tuple3(a,b),
tuple3(b,c),
tuple4(b,a),
tuple4(b,f(b,a)),
tuple4(c,b),
tuple4(c,f(c,b)),
tuple4(f(a,b),a),
tuple4(f(a,b),f(b,a)),
tuple4(f(b,a),b),
tuple4(f(b,a),f(f(b,c),a)),
tuple4(f(b,c),b),
tuple4(f(b,c),f(c,b)),
tuple4(f(c,a),c),
tuple4(f(c,b),c),
tuple4(f(c,b),f(f(c,a),b)),
tuple4(f(f(α_0,α_1),α_2),f(α_0,f(α_1,α_2))),
tuple5(α_0,α_1,α_2),
tuple6(b,f(a,b),a),
tuple6(b,f(b,a),f(a,b)),
tuple6(c,f(b,c),b),
tuple6(c,f(c,b),f(b,c)),
tuple6(α_0,f(f(α_0,α_1),α_2),f(α_0,α_2)),
tuple6(α_0,f(α_0,f(α_1,α_2)),f(f(α_0,α_1),α_2)),
tuple6(α_0,f(α_0,α_1),f(α_0,f(α_1,α_2))),
}
o(α_0,α_1,α_2)
{
List(b, c, a),
List(c, a, b)
}


grammars(1) (size 33) is:

{
tuple1(a),
tuple1(b),
tuple1(c),
tuple2(b,a,f(b,c),a),
tuple2(b,c,b,f(c,a)),
tuple2(c,a,c,f(a,b)),
tuple2(c,b,f(c,a),b),
tuple3(a,b),
tuple3(b,c),
tuple4(f(a,b),a),
tuple4(f(a,b),f(b,a)),
tuple4(f(b,a),f(f(b,c),a)),
tuple4(f(b,c),b),
tuple4(f(b,c),f(c,b)),
tuple4(f(c,a),c),
tuple4(f(c,b),f(f(c,a),b)),
tuple4(f(f(b,c),a),f(b,f(c,a))),
tuple4(f(f(c,a),b),f(c,f(a,b))),
tuple4(f(α_0,α_1),α_0),
tuple4(α_0,f(α_0,α_1)),
tuple4(α_0,α_1),
tuple5(b,c,a),
tuple5(c,a,b),
tuple6(b,f(b,c),f(b,f(c,a))),
tuple6(b,f(b,f(c,a)),f(f(b,c),a)),
tuple6(b,f(f(b,c),a),f(b,a)),
tuple6(c,f(c,a),f(c,f(a,b))),
tuple6(c,f(c,f(a,b)),f(f(c,a),b)),
tuple6(c,f(f(c,a),b),f(c,b)),
tuple6(α_0,f(α_0,α_1),f(α_1,α_0)),
tuple6(α_0,f(α_1,α_0),α_1),
}
o(α_0,α_1)
{
List(b, a),
List(c, b)
}

grammars(1) yields minimized cut-formula:

∀α_0.∀α_1.(α_1=α_0∨¬α_0=f(α_0,α_1)∨¬f(α_0,α_1)=f(α_1,α_0)∨¬f(α_1,α_0)=α_1)

which is (almost) antisymmetry of the partial order x \leq y iff f(x,y)=x

2015-11-02

grammars(0) and grammars(1) can be combined to the following grammar G_2 of size 27 which
has the same language:

{
tuple1(a),
tuple1(b),
tuple1(c),
tuple2(b,a,f(b,c),a),
tuple2(c,b,f(c,a),b),
tuple2(α_0,α_1,α_0,f(α_1,α_2)),
tuple3(a,b),
tuple3(b,c),
tuple4(f(a,b),a),
tuple4(f(a,b),f(b,a)),
tuple4(f(b,a),f(f(b,c),a)),
tuple4(f(b,c),b),
tuple4(f(b,c),f(c,b)),
tuple4(f(c,a),c),
tuple4(f(c,b),f(f(c,a),b)),
tuple4(f(f(α_0,α_1),α_2),f(α_0,f(α_1,α_2))),
tuple4(f(α_0,α_2),α_0),
tuple4(α_0,f(α_0,α_2)),
tuple4(α_0,α_2),
tuple5(α_0,α_1,α_2),
tuple6(α_0,f(f(α_0,α_1),α_2),f(α_0,α_2)),
tuple6(α_0,f(α_0,f(α_1,α_2)),f(f(α_0,α_1),α_2)),
tuple6(α_0,f(α_0,α_1),f(α_0,f(α_1,α_2))),
tuple6(α_0,f(α_0,α_2),f(α_2,α_0)),
tuple6(α_0,f(α_2,α_0),α_2),
}
o(α_0,α_1,α_2)
{
List(b, c, a),
List(c, a, b)
}

Note that G_2 is not minimal, the following grammar G_3 has size 21 and is obtained from G_2 by abstracting
existing lhs-production rules:

{
(*) tuple1(α_2),
tuple1(c),
(***) tuple2(α_0,α_2,f(α_0,α_1),α_2),
tuple2(α_0,α_1,α_0,f(α_1,α_2)),
(**) tuple3(α_2,α_0),
(**) tuple4(f(α_2,α_0),α_2),
(**) tuple4(f(α_2,α_0),f(α_0,α_2)),
(***) tuple4(f(α_0,α_2),f(f(α_0,α_1),α_2)),
tuple4(f(c,a),c),
tuple4(f(f(α_0,α_1),α_2),f(α_0,f(α_1,α_2))),
tuple4(f(α_0,α_2),α_0),
tuple4(α_0,f(α_0,α_2)),
tuple4(α_0,α_2),
tuple5(α_0,α_1,α_2),
tuple6(α_0,f(f(α_0,α_1),α_2),f(α_0,α_2)),
tuple6(α_0,f(α_0,f(α_1,α_2)),f(f(α_0,α_1),α_2)),
tuple6(α_0,f(α_0,α_1),f(α_0,f(α_1,α_2))),
tuple6(α_0,f(α_0,α_2),f(α_2,α_0)),
tuple6(α_0,f(α_2,α_0),α_2),
}
o(α_0,α_1,α_2)
{
List(b, c, a),
List(c, a, b)
}

(*) abstraction by one variable
(**) abstraction using two variables - could have been obtained in grammars(1) already
(***) abstraction using three variables - could have been obtained in grammars(0) already

