Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Ternary is not Kleene #2958

Merged
merged 3 commits into from
Oct 29, 2021
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
2 changes: 1 addition & 1 deletion RationaleMCP/0034/ReadMe.md
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ A prototype has been implemented in a development version of Wolfram SystemModel
### Experience with Prototype
Although introducing a new built-in type is a change that ammounts to a large number of smaller changes, finding the places in a code base that need attention is easy due to the similarity between `Ternary` and `Boolean`. In a similar way, the implicit conversion from `Boolean` to `Ternary` is a feature that can be implemented by glancing at the handling of implicit conversion from `Integer` to `Real`.

Regarding the application of this MCP to a new attribute called `visible` in the `Dialog` annotation, the proposed choice of Kleene logic certainly gets the job done. The default value of `unknown` which means _apply tool-specific rules for visibility_, a user can easily write a ternary logical expression to override the default in either way, and the expression may also evaluate to `unknown` in cases where the user doesn't want to fall back on the tool logic. Thanks to the implicit cast from `Boolean`, most uses of `visible` would probably be in the simple forms `visible = true` or `visible = false`. However, upon closer acquaintance with the Kleene logic, which still appears as the most natural choice for `Ternary`, it has been questioned whether this is the best way to model the absence of information, see [rationale](rationale.md#The-option-type-alternative).
Regarding the application of this MCP to a new attribute called `visible` in the `Dialog` annotation, the proposed choice of defining `not`, `and` and `or` in accordance with Kleene logic certainly gets the job done. The default value of `unknown` which means _apply tool-specific rules for visibility_, a user can easily write a ternary logical expression to override the default in either way, and the expression may also evaluate to `unknown` in cases where the user doesn't want to fall back on the tool logic. Thanks to the implicit cast from `Boolean`, most uses of `visible` would probably be in the simple forms `visible = true` or `visible = false`. However, upon closer acquaintance with the Kleene logicwhich still appears as the most natural basis for defining the logical connectives for `Ternary` it has been questioned whether this is the best way to model the absence of information, see [rationale](rationale.md#The-option-type-alternative).

## Required Patents
To the best of our knowledge, there are no patents that would conflict with the incorporation of this MCP.
Expand Down
6 changes: 3 additions & 3 deletions RationaleMCP/0034/rationale.md
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ Even though the use of option types could be restricted to `Boolean` to start wi
Another advantage of introducing option types instead of `Ternary` would be that it would probably be acceptable to say that no option type can be used for indexing into arrays. This would simplify parts of the implementation compared to `Ternary`.

However, these are some reasons for sticking with `Ternary` instead of `Boolean?`:
- If the usual ternary logic according to Kleene is what we want — which is the assumption of this MCP — the use of `Boolean?` would imply an unnatural interpretation of `none`. [This argument is elaborated below.](#Using-none-to-represent-undefined)
- If the usual ternary operators `not`, `and` and `or` in accordance with Kleene is what we want — which is the assumption of this MCP — the use of `Boolean?` would imply an unnatural interpretation of `none`. [This argument is elaborated below.](#Using-none-to-represent-undefined)
- Introducing the literal `none` to refer to the absence of a value for an option type leads to a significant change of the Modelica type system, as `none` can have any option type. Even if type inference would be implemented, there would be problems when it comes to implicit conversions (see above).
- Explicitly writting out the type of a _none_ as in `Boolean?()` would be inconvenient compared to just saying `unknown`. (However, it would then be natural to define implicit conversion to any option type.)
- Attributes of other type than `Boolean` typically have a default behavior that can be expressed with a default value (like the empty string in case of `String`), removing the need for an option type to express the absence of a value.
Expand All @@ -87,7 +87,7 @@ However, these are some reasons for sticking with `Ternary` instead of `Boolean?
- It is probably a bad idea to just introduce option types in Modelica without considering the more general concepts that would give option types as a special case. Such more general constructs inspired by MetaModelica have been discussed at many design meetings without getting much traction.

## Using `none` to represent _undefined_
While possible to interpret `Boolean?()` (hereafter referred to as `none` for brevity) as _unknown_ and define logical operation on `Boolean?` in the same way as for `Ternary` to get a Kleene logic, the generalization of this interpretation to other option types such as `Real?` or `String?` isn't as useful. The natural interpretation of `none` would rather be _undefined_, which leads to more useful generalizations to other option types.
While possible to interpret `Boolean?()` (hereafter referred to as `none` for brevity) as _unknown_ and define logical operation on `Boolean?` in the same way as for `Ternary` to get consistency with Kleene logic, the generalization of this interpretation to other option types such as `Real?` or `String?` isn't as useful. The natural interpretation of `none` would rather be _undefined_, which leads to more useful generalizations to other option types.

For example, one could define that concatenation with an _undefined_ `String?`, would be a no-op, and the same for addition or multiplication with an _undefined_ `Real?`. For `Boolean?` it would then be natural to define both disjunction and conjunction with _undefined_ to be no-ops, leading to things such as `none and true = some(true)`.

Expand All @@ -104,4 +104,4 @@ Please note that this logical table does not correspond to the often cited four-

For the numeric types `Real` and `Integer`, a better analog to `unknown` would be `NaN` (not-a-number), having very different arithmetic behavior compared to the no-ops of _undefined_. For example, this gives the expected behavior of adding _unknown_ to any number resulting in _unknown_.

To summarize, while option types have many interesting applications — including modeling of built-in attributes with non-trivial defaults — it would be a mistake to use `Boolean?` for the usual ternary logic according to Kleene with _unknown_ as the third truth value. This also shows that `Ternary` is not going to become redundant if option types are added to Modelica in the future.
To summarize, while option types have many interesting applications — including modeling of built-in attributes with non-trivial defaults — it would be a mistake to use `Boolean?` for the usual ternary connectives defined in accordance with Kleene. This also shows that `Ternary` is not going to become redundant if option types are added to Modelica in the future.
4 changes: 3 additions & 1 deletion RationaleMCP/0034/ternary.md
Original file line number Diff line number Diff line change
Expand Up @@ -32,10 +32,12 @@ There is a total order of the possible `Ternary` values given by `Ternary(false)

## Expressions with Ternary

Logical operations on `Ternary` are defined according to Kleene, where `unknown` can be thought of as representinc uncertainty about being `true` or `false`. With this interpretation the Kleene logic tables then follow from the Boolean logic.
The logical connectives `not`, `and` and `or` on `Ternary` are defined in accordance with Kleene, where `unknown` can be thought of as representinc uncertainty about being `true` or `false`. With this interpretation the truth tables then follow from the Boolean logic.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Regarding comment in main MCP issue:

Right. We should not use Ternary to build theorem proofers.

But our users will see the 3-valued logic, and start trying it on more complex domains than just dialog visibility. I have this requirements engineering library of EDF in my mind that had been proposed some time ago, also as a motivation to add 3-valued logic (at the end it turned out it was kind of a 4-valued logic because of the need to model time ... voilà, there it goes). With the proposed 3-valued logic, this requirements engineering example will first become sort-of more easy to develop, but then turns out to fall short and then all the craziness comes in step by step as additional requirements and corner-cases.

Your comment makes me think of the connectives I would have liked to handle things like "Boolean annotations with clever automatic default". Instead of interpreting unknown as unknown, I would have liked it to be interpreted as disregard, allowing it to be cancelled from both conjunction and disjunction. That is, instead of and and or, I would have wanted the connectives duand (disregard-unknown-and) and duor (disregard-unknown-and). Do you happen to know if this has a name in the literature? If so, maybe this could also be mentioned non-normatively, as it illustrates that not even the truth tables for and and or are as obvious as one might first think?


For example, to evaluate `false or unknown`, one has to consider both possible outcomes for the uncertain operand, meaning that the result might be ither `false or false` or `false or true`. Since the different outcomes don't agree, the result of the operation is uncertain, represented by `unknown`.

Although the truth tables of `not`, `and` and `or` agree with Kleene logic, the set of logical connectives on `Ternary` is deliberately not meant to model any particular ternary logic. In particular, by not defining an operator for material implication, `Ternary` cannot be considered a complete model of Kleene logic. Applications requiring a complete model of one of the many possible ways to define ternary logic may use `Ternary` to represent the three truth values, but should define all the logical connectives of the logic in question as a package (library) of functions.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This paragraph relates to this comment in the main MCP issue:

To reassure you that the MCP is not about a 3-valued logic as you think of it, note that the MCP does not introduce an implies operator

The Kleene truth tables of the MCP already define implication (since implication in Kleene is just ¬A ∨ B). The issues of this logic are there, regardless if we support a dedicated implication operator or not. The point of these issues I described above is not that Kleene is wrong or something. The issue is that complex expressions in that logic often yield very surprising results (for which reason other, more advanced logics are proposed). More complex 3-valued logic relations may be hard to develop and likely boil down to try and error for users or need for step-by-step debugging of logic expressions.

So, while I agree that implication in Kleene is ¬A ∨ B, I wouldn't call something Kleene logic until this definition has been made.


Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(Attaching comment to empty line just to get a separate discussion thread.) The paragraph, meant to turn into non-normative text in the specification also tries to address this concern from the main MCP issue:

the MCP does not intend to enter the muddy waters of all 3-valued logics

And I don't want it to be the opener for future proposals in that direction.

If we say: That's it, Kleene truth tables and nothing more -- even if hell freezes -- I am very much Ok with it. The Kleene 3-valued logic is the most simple straight forward many-valued logic. I consider it very limited in its application area however -- that is why it is not used for anything but most simple applications. If somebody comes in the future with "but that case of the three-valued logic also needs some consideration" we should pull the plug.

I believe it will be hard to specify things in a way that will for sure prevent more or less arbitrary future specialization to some popular ternary logic, but I think that a well formulated non-normative paragraph or two should be able to capture the essence of the concerns felt today, and thereby drastically reduce risk of these concerns being forgotten or ignored in the future.

### Unary operators
Unary operators on `Ternary`, where `x` is an expression of type `Ternary`:

Expand Down