Add negated premises

[nomeata]

This is necessary to express the actual meaning of the otherwise premises.

[rossberg]

My sense still is that it ought to be enough to only negate Boolean formulas, not inductive premises. That would seem much simpler.

[nomeata]

But side conditions can be arbitrary premises, including predicates. So if one has to negate them, one has to negate predicates. I don't see how you get around that.

At least not without a fair number of rather arbitrary restrictions on the input (“In the rule before a rule with otherwise only boolean premises can be used”).

And at least for the proof backends, the ability to negate predicate side conditions is precisely what you need to implement else in greatest possible generality. (The only restriction I think being that the predicate that uses else can't be recursive, as that wouldn't be well-defined in general.)

[nomeata]

An alternative might be to simplify premises to only allow (boolean) expressions, and add a constructor to Expressions for “call a predicate (as a boolean function)”. This would be a great fit for the Isabelle backend and arguably also for the math backend. The lean and Coq backends would have to do a bit of work to distangle Prop from real Bool.

[rossberg]

At least not without a fair number of rather arbitrary restrictions on the input (“In the rule before a rule with otherwise only boolean premises can be used”).

Yes, that's the restriction I have in mind. I wouldn't call it arbitrary. We certainly do not use anything more general.

[nomeata]

Yes, that's the restriction I have in mind. I wouldn't call it arbitrary. We certainly do not use anything more general.

Well, in that case let’s add NegatedPr as we do here, and just don’t use it with non-boolean premises in the source spec (but give the ir-to-ir passes the option of doing so if it is helpful) and move on?

[rossberg]

But then wouldn't it just be redundant? The IL will be affecting almost every backend, so I'd be a bit reluctant to add something semantically complex prematurely, before we know it's really needed.

[nomeata]

Well, some backends need it, at least at the moment. All other backends can just error out when they encounter something they don’t want to handle – just as they can do if other invariants like “In the rule before a rule with otherwise only boolean premises can be used” are violated.

I don’t see why “Some backends cannot handle non-boolean premises in negation” is so much more dubious than the existing the “Some backends cannot handle non-boolean premises in rules before a rule with otherwise”

[nomeata]

I don’t see much wrong with the following examples, and even if we don't use it right away, wouldn’t go out of my way to not support it:

Otherwise referring to rules with not syntactic different lhs:

relation Step: expr -> expr

rule Step_is_null1:
  (is_null 0) -> True
rule Step_is_null2:
  (is_null n) -> False
  -- otherwise

and possibly also rules using relations in side conditions:

relation Even : Even expr
rule Even_0:
  Even 0
rule Even_SS:
  Even (S (S n))
  -- Even n

rule Step_is_even1:
  (is_even n) -> True
  -- Even n
rule Step_is_even2:
  (is_even n) -> False
  -- otherwise

---

I’m surprised this is so contentious, so probably there is a deeper misunderstanding on my side here. Maybe @conrad-watt sees why we are talking past each other here, and can clarify?

(Maybe the “issue“ is that the reduction relation is supposed to be “executable” and thus can’t use Prop-valued predicates, only bool-valued predicates, in side condition. And although it’s defined using the machinery of inductive rules, it’s really conceptually a function definition, where try-rule-in-order is much more common.)

[rossberg]

(Maybe the “issue“ is that the reduction relation is supposed to be “executable” and thus can’t use Prop-valued predicates, only bool-valued predicates, in side condition. And although it’s defined using the machinery of inductive rules, it’s really conceptually a function definition, where try-rule-in-order is much more common.)

That's certainly part of the reason. I would also think that the meta-theory of negation in Prop is more involved than for Bool, at least in some theories. Doesn't it build in an assumption about a classical interpretation?

All other backends can just error out when they encounter something they don’t want to handle

I don't think that's a route we should consider. The IL better be clearly defined and not up to different interpretation from different backends. The respective assumptions should be manifest in IL validation. Besides principle reasons, that's to ensure that middlend passes are (and remain) compatible with backends.

I rather suggest that we explicitly rule out the use of otherwise on non-Boolean conditions, and have that checked in both elaborator and validator.

[nomeata]

Doesn't it build in an assumption about a classical interpretation?

No more than non-negated relation premises in an “executable” reduction relation, I'd say.

[nomeata]

Cross-reference relevant discussion: https://github.com/orgs/Wasm-DSL/discussions/11#discussioncomment-5976200