Changes to Logical classes

[lgeretti]

Originally reported by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)

---

Currently our Logical classes are templates parametrised by a Paradigm tag, with typedefs to user-level names (Boolean, Sierpinskian, Kleenean). I plan to re-implement so that the user-level names are class names, and make some other changes to the semantics to make the interface slightly cleaner.

1. Use Boolean, Sierpinskian and Kleenean as top-level class names, with Lower/Upper- modifiers for Kleenean, Negated- for Sierpinskian, and Validated- and Approximate- versions. Here, Kleenean is a completion of Boolean in much the same way as Real is a completion of Rational.

2. Distinguish Sierpinskian from LowerKleenean. Sierpinskian would be for cases in which there is no possibility for robust falsification (which in our case is essentially for inequality) and LowerKleenean for partial information on a quasidecidable predicate (e.g. testing for positivity of a LowerReal, where positivity of a Real would return Kleenean).

   • One of the main conceptual motivations for this change is on whether 'Sierpinskian' with values 'true' and 'indeterminate' has more or less information (i.e. can be converted to/from) 'Kleenean' with values 'true', 'indeterminate' and 'false'. Conversion by inclusion Sierpinskian -> Kleenean loses the information that 'false' is not a possible value, whereas conversion Kleenean -> Sierpinskian taking 'false' to 'indeterminate' loses the information when the value is false.
   • After the change, there would then be implicit conversions Sierpinskian -> Kleenean -> LowerKleenean.

3. Fix LowerKleenean to be for Verifyable predicates (currently LowerKleenean is for Falsifyable, but this is incorrect, since a verified lower bound of 'true' means the predicate must be true, but a lower bound of 'false' means no information).

4. Effective logical classes will not be convertible to Validated/Approximate classes, but can only be checked with some given Effort.

   • Mixed Effective/Validated operations could be supported by storing the effort_used in the Validated class, and using this to check(...) the Effective value (see below).

5. Add conjunction/disjunction for Sequences of logical types.

6. Our SetInterface classes also need Effective and Validated versions. Effective (i.e. exactly specified sets) would have predicates returning (Lower)Kleenean, and Validated sets return their Validated logical versions.

7. Store the effort_used for a Validated/Approximate logical value, to allow mixed Effective/Validated operations (see above).

8. Store a cached Validated checked value together with the Effort used with any Effective logical predicate. The advantage of this is fast re-checking of predicates.

   • We need to decide on whether to maintain functionality e.g. if p is a Kleeanean and p.check(Effort(1)) yields indeterminate and p.check(Effort(3)) yields true, should a subsequent p.check(Effort(1)) yield true or indeterminate? What about p.check(Effort(2))?
   • I think that maintaining functionality is sufficiently important to do so. This can be accomplished by also storing the largest Effort for which no decision is reached. Recomputation would only be needed for an intermediate Effort.

Additionally:

9. Consider removing possibly(...) and definitely(...) for Approximate and Naive logical values, as these always yield true and false. (However, the usage is consistent, so may be useful in template code.)
10. Deprecate use of decide(...). It currently has two orthogonal uses: check Effective logical types with minimum Effort, and select an appropriate case for Validated (definitely) and Approximate (probably). Maybe rename to something less snappy, like cast_decision.
11. Consider changing probably to is_likely and adding an is_unlikely. Consider changing these to only apply to Approximate logical types.

---

• Bitbucket: https://bitbucket.org/ariadne-cps/development/issue/12

[lgeretti]

Original comment by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)

---

I've updated the docs; hope this answers your questions.

[lgeretti]

Original comment by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)

---

Some questions:

1. The relationship between Approximate and Naive is not so clear from the doc. Does for example ApproximateKleenean relate to NaiveKleenean as ValidatedKleenean does to Kleenean?

2. I do not understand when a method should return an Effective type rather than a Validated one.

3. When can we neglect to specify the Effort, if we return a Validated type?

[lgeretti]

Original comment by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)

---

I've made a first implementation (in working-logical) including documentation; please let me know what you think.

The implementation uses custom classes at the user level rather than templates and typedefs. However, there are some generic constructs in use here, and it may be worth seeing to what extent these can be exploited:

• Kleenean is OrderCompletion, just as Real is an Order/MetricCompletion.
• We have Lower/Upper classes, just as Lower/Upper, and a Negated.
• We have a relationship between Effective, Validated and Approximate classes.

[lgeretti]

Original comment by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)

---

I am favorable to a more detailed definition of the logical classes and their enforcement throughout the library. So every development towards it is welcome. In general I am against typedefs, so custom classes are ok with me. Could you use this chance to write down a strong definition of their semantics in the API docs, when you write the classes? I am still at a loss regarding their specific role within the library, and a good hint on their proper usage would be nice.

[lgeretti]

What is the status of this issue?