Strange behavior of lambda equality

[jad-hamza]

f1 and f2 should be equal here. It looks like that the imperative cleanup transformation replaces plus(Zero(), Zero()) by u in f2. For Stainless, u and plus(Zero(), Zero()) don't have the same structure so the assertion that f1 is different than f2 succeeds.

Also, in general, don't we want (x: Nat) => plus(Zero(),Zero()) and (x: Nat) => u to be considered as the same function?

import stainless.lang._
import stainless.annotation._

object Equality {
  sealed abstract class Nat
  case class Zero() extends Nat 
  case class Succ(n: Nat) extends Nat

  def plus(a: Nat, b: Nat): Nat = a match {
    case Zero() => b
    case Succ(a2) => Succ(plus(a2,b))
  }

  def theorem(a: Nat) = {
    val f1 = (x: Nat) => plus(Zero(), Zero())
    val u = plus(Zero(), Zero())
    val f2 = (x: Nat) => plus(Zero(), Zero())
    assert(f1 != f2) // VALID
  }
}

Result after transformation by imperative.cleanup, probably due to the call to simplifyLets.

def theorem(a: Nat): Unit = {
  val f1: (Nat) => Nat = (x: Nat) => plus(Zero(), Zero())
  val u: Nat = plus(Zero(), Zero())
  val f2: (Nat) => Nat = (x: Nat) => u
  assert(f1 ≠ f2)
  ()
}

[samarion]

I'll have to take a look at what imperative is doing here. I can also take a look at https://github.com/epfl-lara/stainless/issues/30 while I'm at it.

About equality, we can't say that (x: Nat) => plus(Zero(),Zero()) and (x: Nat) => u are equal in general because of potential non-termination in plus. Namely, running

val u = plus(Zero(), Zero())
val f = (x: Nat) => u

may non-terminate whereas

val f = (x: Nat) => plus(Zero(), Zero())

will always terminate. However, if both lambdas were pure, some structural rewriting would occur and make them equal. It might be interesting for Inox to have a pure mode where all expressions are considered pure (this would make sense when it's a backend to Stainless).

This mode could maybe also support removing assertions for the let simplifications we had talked about. However, if I remember correctly I had looked into implementing such a mode and it was non-trivial due to how the Inox code is structured... I'll take a look again.

[jad-hamza]

There are three variants that we can consider separately:

Variant 1 (the one you wrote)

((x: Nat) => plus(Zero(), Zero())) ==
{
  val u = plus(Zero(), Zero())
  (x: Nat) => u
}

Variant 2 (the one corresponding to defining u first, then checking equality (this one corresponds to the Stainless code above I think) :

val u = plus(Zero(), Zero())
((x: Nat) => plus(Zero(), Zero())) == ((x: Nat) => u)

Variant 3, where u is defined locally to the lambda that uses it

((x: Nat) => plus(Zero(), Zero())) == {
  (x: Nat) => {
    val u = plus(Zero(), Zero())
    u
  }
}

According to the semantics of the logic that Inox uses and to the definition of equality, are these formulas valid (semantically)? I think it's ok for Inox to return UNKNOWN if proving that they are valid is too difficult, but I'm afraid that saying that the formulas are valid when we replace == by != might lead to inconsistencies.

Also, do we want the two following programs to be valid, or invalid (from a semantic/logic point of view)? The first one passes, the second one returns a counter-example. In the formal logic underlying Inox, how to define equality?

  def equalFunctions(a: Nat, b: Nat) = {
    require(a == b)

    ((x: Nat) => a) == ((x: Nat) => b)
  } holds

  def extensionality(f: Nat => Nat, g: Nat => Nat) = {
    require(forall((x: Nat) => f(x) == g(x)))

    f == g
  } holds

[samarion]

The only semantics Inox is aware of are the operational semantics associated to Inox programs. Function equality must therefore be computable. Structure-based equality is and that's why we use this, even though it doesn't correspond to the usual notion of equality used in HOL.

In practice, due to the many code transformations that Inox and Stainless use, limiting equality to the exact structure of closures encountered by the solver is limiting and can lead to unexpected results. The equality notion we use is therefore slightly more complex than structural equality and goes through a normalization of the closure first (still computable). This is why (x: Nat) => plus(Zero(), Zero()) and (x: Nat) => u could be considered equal if plus is pure. However, (x: Nat) => f(x) and (x: Nat) => g(x) will never be equal for f != g even when f(y) == g(y) for all y. If you want extensional equality, you can always explicitly use such a predicate that involves quantifiers since those kind of break operational semantics anyways.

Note that since the notion of equality used by the solver corresponds exactly to the one used by the evaluator, there is no risk of inconsistency here. The notion is simply not consistent with HOL semantics. However, Inox supports custom equality operators so we could introduce HOL functions that use extensional equality as a library if we need them.

On Tue, Jul 25, 2017 at 2:01 PM, Jad notifications@github.com wrote:

There are three variants that we can consider separately:

Variant 1 (the one you wrote)

((x: Nat) => plus(Zero(), Zero())) == { val u = plus(Zero(), Zero()) (x: Nat) => u }

Variant 2 (the one corresponding to defining u first, then checking equality (this one corresponds to the Stainless code above I think) :

val u = plus(Zero(), Zero()) ((x: Nat) => plus(Zero(), Zero())) == ((x: Nat) => u)

Variant 3, where u is defined locally to the lambda that uses it

((x: Nat) => plus(Zero(), Zero())) == { (x: Nat) => { val u = plus(Zero(), Zero()) u } }

According to the semantics of the logic that Inox uses and to the definition of equality, are these formulas valid (semantically)? I think it's ok for Inox to return UNKNOWN if proving that they are valid is too difficult, but I'm afraid that saying that the formulas are valid when we replace == by != might lead to inconsistencies.

Also, do we want the two following programs to be valid, or invalid (from a semantic/logic point of view)? The first one passes, the second one returns a counter-example. In the formal logic underlying Inox, how to define equality?

def equalFunctions(a: Nat, b: Nat) = { require(a == b)

((x: Nat) => a) == ((x: Nat) => b)

} holds

def extensionality(f: Nat => Nat, g: Nat => Nat) = { require(forall((x: Nat) => f(x) == g(x)))

f == g

} holds

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/62#issuecomment-317716127, or mute the thread https://github.com/notifications/unsubscribe-auth/ADKzhAFXDbiSywN9ETaBQkjgd7RfGHlKks5sRdkWgaJpZM4Ohk-Z .

[jad-hamza]

If I understand correctly, all threes variants are invalid for the operational semantics of Inox (and valid if we replace == by !=)? About the inconsistency, I'm afraid specifically about the interaction with equalFunctions, which is valid.

[samarion]

Yes, all three variants are invalid (and valid for !=).

You can't use equalFunctions to show that (x: Nat) => plus(Zero(), Zero()) == (x: Nat) => u. You have (x: Nat) => u equal to (x: Nat) => v iff u == v, but equalFunctions(plus(Zero(), Zero()), u) won't imply (x: Nat) => plus(Zero(), Zero()) == (x: Nat) => u, but rather that

val v = plus(Zero(), Zero())
(x: Nat) => u == (x: Nat) => v

On Tue, Jul 25, 2017 at 2:59 PM, Jad notifications@github.com wrote:

If I understand correctly, all threes variants are invalid for the operational semantics of Inox (and valid if we replace == by !=)? About the inconsistency, I'm afraid specifically about the interaction with equalFunctions, which is valid.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/62#issuecomment-317729415, or mute the thread https://github.com/notifications/unsubscribe-auth/ADKzhLGHIz1Mqa9r_2UQGVnRN_9l7DKSks5sRea8gaJpZM4Ohk-Z .

[jad-hamza]

Hmm I see, that's funny

By the way, is this the code responsible for the strange behavior of the expression being replaced by the variable? https://github.com/epfl-lara/inox/pull/31 I wonder if removing that case breaks anything else?

[samarion]

Probably not in Inox, but I'll have to run the Stainless regression on it to be sure, that's where most bugs appear. You can run Inox tests with "sbt test it:test" (~5min) and same in Stainless once you make the build file point to your local Inox (but be warned, this takes about 45 minutes without the parallelism we get on the server).

On Tue, Jul 25, 2017 at 3:25 PM, Jad notifications@github.com wrote:

Hmm I see, that's funny

By the way, is this the code responsible for the strange behavior? epfl-lara/inox#31 https://github.com/epfl-lara/inox/pull/31 I wonder if removing that case breaks anything else?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/62#issuecomment-317736397, or mute the thread https://github.com/notifications/unsubscribe-auth/ADKzhE8Yi3_cNMjFiJVX9faQncbQdFXlks5sRezmgaJpZM4Ohk-Z .

[jad-hamza]

From these examples, we can deduce that a formula F with a free variable x: Nat can be proven valid (or return true as a function), while the formula [t / x]F (where x is substituted by a term t: Nat) can be invalid (or return false as a function). In particular this may happen when t involve recursive functions, due to t not being "pure", is that right?

(In the examples above, x is u, and t is plus(Zero,Zero))

[samarion]

Yes, that's true. However, you shouldn't view Inox models as substitutions but as let-bindings. Given a model M, M(p) corresponds to the expression val x1 = M(x1); ...; val xn = M(xn); p. In that case, validity is preserved by "substitution". Also, given the normalization used for lambda equality, if t in your example is a value, then validity is preserved.

On Tue, Jul 25, 2017 at 3:44 PM, Jad notifications@github.com wrote:

From these examples, we can deduce that a formula F with a free variable x: Nat can be proven valid (or return true as a function), while the formula [t / x]F (where x is substituted by t / x) can be invalid (or return false as a function). In particular this may happen when t involve recursive functions, due to t not being "pure", is that right?

(In the examples above, x is u, and t is plus(Zero,Zero))

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/62#issuecomment-317741507, or mute the thread https://github.com/notifications/unsubscribe-auth/ADKzhDt2mTHt_z1_eurdka8Fxo_4Enmcks5sRfEogaJpZM4Ohk-Z .

[samarion]

Fixed by https://github.com/epfl-lara/inox/pull/31

[jad-hamza]

To continue about equality, it looks like that it's not a congruence relation, is that ok?

And with this definition there are some consequences on Stainless. If a property is valid, it can become invalid after adding @inline annotations (or vice versa). Are there known examples where @inline break besides the ones using equality?

Also, are there other things that are known to break the substitution property besides this definition of equality?

By the way, in the Inox code, where can I see how equality is evaluated (in the operational semantics)? Is it the Equals case in the RecursiveEvaluator? Thanks

[samarion]

I believe this remains a congruence relation. There is no way to compute two different results given equal lambdas. How could it not be congruent?

About @inline, there could indeed be some impact if you are relying on function disequality to show validity of some property and after adding @inline the two functions could become equal. However, if you are relying on disequality based on structure to prove some property, you had better understand lambda equality quite well! I can't think of any other case where @inline would impact equality.

About substitutions, substituting with terms just doesn't make sense to me in the context of expressions. You could just substitute with a non-terminating function call or even assert(false). What would such substitutions mean regarding validity? I view validity as holding for arbitrary inputs, and inputs to programs/expressions can only be values (which can't change lambda equality).

The equals case is indeed where equality is evaluated, but to avoid having to recursively check equality of sub-expressions, equality is reduced to AST equality by making sure all values are in some normal form. The normalization of lambda terms takes place in the Lambda case in the RecursiveEvaluator.

On Thu, Jul 27, 2017 at 11:13 AM, Jad notifications@github.com wrote:

To continue about equality, it looks like that it's not a congruence relation, is that ok?

And with this definition there are some consequences on Stainless. If a property is valid, it can become invalid after adding @inline https://github.com/inline annotations (or vice versa). Are there known examples where @inline https://github.com/inline break besides the ones using equality?

Also, are there other things that are known to break the substitution property besides this definition of equality?

By the way, in the Inox code, where can I see how equality is evaluated (in the operational semantics)? Is it the Equals case in the RecursiveEvaluator? Thanks

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/62#issuecomment-318306083, or mute the thread https://github.com/notifications/unsubscribe-auth/ADKzhO01bKW9EBUODgjsr9-WRpUckvofks5sSFS_gaJpZM4Ohk-Z .

[jad-hamza]

For equality to be a congruence, don't we need it to respect the structure of the terms (lifting equality)? So u = Plus(Zero,Zero) would imply ((x: Nat) => u) = ((x: Nat) => Plus(Zero,Zero)).

For substitutions, I'm thinking that formally, there is a logical judgement that says: Given a context Gamma that assigns (unknown) variables to types, and a context Sigma that (known) variables to terms, a formula F is valid (for Inox), or Gamma, Sigma |- F valid.

If I understand correctly, for Inox, this judgement is defined in terms of the operations semantics in RecursiveEvaluator. More precisely, we have Gamma, Sigma |- F valid iff for all possible values v1,...,vn, the expression [v1,...,vn / Gamma] F evaluates to true under context Sigma. Is the expression [v1,...,vn / Gamma] F allowed to diverge and not return anything (e.g. in presence of non-terminating terms)?

Evaluating a forall requires a similar definition right? The expression forall((x: T) => e) evaluates to true if for any value v: T, [x/v] e evaluates to true.

[jad-hamza]

For @inline, this is an example of a program that is verified valid with the annotation but there is a counter-example without the annotation. (Similarly, we can make something that is valid without the annotation but invalid with the annotation)

import stainless.lang._
import stainless.annotation._

object Equality {
  sealed abstract class Nat
  case class Zero() extends Nat 
  case class Succ(n: Nat) extends Nat

  def plus(a: Nat, b: Nat): Nat = a match {
    case Zero() => b
    case Succ(a2) => Succ(plus(a2,b))
  }

  @inline // the program is VALID when this is there, but INVALID when it's not
  def v() = plus(Zero(), Zero())

  def theorem(a: Nat) = {
    assert(((x: Nat) => plus(Zero(), Zero())) == ((x: Nat) => v))
  }
}

[samarion]

I don't think it has to respect the structure of the terms, only the structure of the relevant relations (namely evaluation since everything else is defined with respect to it). I guess it isn't congruent with respect to term composition or construction but that doesn't seem like a very useful property for expressions (maybe more so for formulas, I'm not sure).

The judgment is indeed defined in terms of the operational semantics and ensures that the expression will not evaluate to false under value substitutions. However, I don't really understand where the Sigma is coming from. Why would we consider some context mapping variables to arbitrary terms (expressions)?

Evaluating a forall is still a gray zone. But indeed, it is something along the lines of what you stated. So considering only value substitutions.

On Thu, Jul 27, 2017 at 1:31 PM, Jad notifications@github.com wrote:

For equality to be a congruence, don't we need it to respect the structure of the terms (lifting equality)? So u = Plus(Zero,Zero) would imply ((x: Nat) => u) = ((x: Nat) => Plus(Zero,Zero)).

For substitutions, I'm thinking that formally, there is a logical judgement that says: Given a context Gamma that assigns (unknown) variables to types, and a context Sigma that (known) variables to terms, a formula F is valid (for Inox), or Gamma, Sigma |- F valid.

If I understand correctly, for Inox, this judgement is defined in terms of the operations semantics in RecursiveEvaluator. More precisely, we have Gamma, Sigma |- F valid iff for all possible values v1,...,vn, the expression [v1,...,vn / Gamma] F evaluates to true under context Sigma. Is the expression [v1,...,vn / Gamma] F allowed to diverge and not return anything (e.g. in presence of non-terminating terms)?

Evaluating a forall requires a similar definition right? The expression forall((x: T) => e) evaluates to true if for any value v: T, [x/v] e evaluates to true.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/62#issuecomment-318336258, or mute the thread https://github.com/notifications/unsubscribe-auth/ADKzhGSN5C96SLzUecJPa4sG3tozNP-jks5sSHT3gaJpZM4Ohk-Z .

[samarion]

For the @inline case, I'm not arguing about validity vs invalidity. I'm saying that @inline can only make more things equal, never less. And it can only make things equal that are indeed equal according to HOL function equality semantics. So the only "weird" case is if you're expecting two functions to not be equal due to different structures although they are extensionally equal (as in your example). Such a case sounds a bit strange to me.

On Thu, Jul 27, 2017 at 2:06 PM, Nicolas Voirol voirol.nicolas@gmail.com wrote:

I don't think it has to respect the structure of the terms, only the structure of the relevant relations (namely evaluation since everything else is defined with respect to it). I guess it isn't congruent with respect to term composition or construction but that doesn't seem like a very useful property for expressions (maybe more so for formulas, I'm not sure).

The judgment is indeed defined in terms of the operational semantics and ensures that the expression will not evaluate to false under value substitutions. However, I don't really understand where the Sigma is coming from. Why would we consider some context mapping variables to arbitrary terms (expressions)?

Evaluating a forall is still a gray zone. But indeed, it is something along the lines of what you stated. So considering only value substitutions.

On Thu, Jul 27, 2017 at 1:31 PM, Jad notifications@github.com wrote:

For equality to be a congruence, don't we need it to respect the structure of the terms (lifting equality)? So u = Plus(Zero,Zero) would imply ((x: Nat) => u) = ((x: Nat) => Plus(Zero,Zero)).

For substitutions, I'm thinking that formally, there is a logical judgement that says: Given a context Gamma that assigns (unknown) variables to types, and a context Sigma that (known) variables to terms, a formula F is valid (for Inox), or Gamma, Sigma |- F valid.

If I understand correctly, for Inox, this judgement is defined in terms of the operations semantics in RecursiveEvaluator. More precisely, we have Gamma, Sigma |- F valid iff for all possible values v1,...,vn, the expression [v1,...,vn / Gamma] F evaluates to true under context Sigma. Is the expression [v1,...,vn / Gamma] F allowed to diverge and not return anything (e.g. in presence of non-terminating terms)?

Evaluating a forall requires a similar definition right? The expression forall((x: T) => e) evaluates to true if for any value v: T, [x/v] e evaluates to true.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/62#issuecomment-318336258, or mute the thread https://github.com/notifications/unsubscribe-auth/ADKzhGSN5C96SLzUecJPa4sG3tozNP-jks5sSHT3gaJpZM4Ohk-Z .

[jad-hamza]

Can you expand a bit on the definition of congruence you have in mind? Is it eval(e1 = e2) = true implies eval(e1) = eval(e2)?

So do we want [v1,...,vn / Gamma] F to always evaluate to true, or never evaluate to false? (do we allow non-termination for validity?)

I thought the Sigma would be populated when entering in a let binding? (Would that be the context rctx: RC in the RecursiveEvaluator?)

[jad-hamza]

Equality is defined on "Expr", so for congruence I had in mind this:

e1 = e2 is valid implies Ctx[e1] = Ctx[e2] is valid, where Ctx is an Expr with a hole.

[jad-hamza]

I agree about @inline, it should never make things less equal according to this definition of equality. Do you know of other examples where @inline breaks validity vs invalidity that do not involve equality?

[jad-hamza]

So do we want [v1,...,vn / Gamma] F to always evaluate to true, or never evaluate to false? (do we allow non-termination for validity?)

Nevermind, I misread your comment. So if the definition is that the term never evaluates to false, substituting by a non-terminating term shouldn't break validity right (ignoring this definition of equality)?

[samarion]

The congruence is more like e1 = e2 valid implies that let v = e1 in Ctx = let v = e2 in Ctx is valid. Free variables can only ever be bound to values so it makes more sense to consider lets than substitutions here (or you can consider substitutions with values).

Let bindings evaluate the expression before considering the body so the evaluation context is a mapping from variables to values. Actually, instead of evaluating [v1,...vn / Gamma] F we typically evaluate F under the context [v1,...,vn / Gamma] and this context gets extended when entering let bodies.

We do allow non-termination for validity as Inox doesn't have a termination checker. This is why it would maybe make sense for Inox to consider everything pure and rely on Stainless to actually enforce this. Note that although everything being pure would mean that most of the functions we've discussed would become equal (structure being (x: Nat) => u), we would still have the same problems for functions that use the argument x.

For @inline, I don't know of any other cases where it could change validity. I think that lambdas are the only case where the structure of the term is actually important.

On Thu, Jul 27, 2017 at 2:17 PM, Jad notifications@github.com wrote:

Can you expand a bit on the definition of congruence you have in mind? Is it eval(e1 = e2) = true implies eval(e1) = eval(e2)?

So do we want [v1,...,vn / Gamma] F to always evaluate to true, or never evaluate to false? (do we allow non-termination for validity?)

I thought the Sigma would be populated when entering in a let binding? (Would that be the context rctx: RC in the RecursiveEvaluator?)

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/62#issuecomment-318345322, or mute the thread https://github.com/notifications/unsubscribe-auth/ADKzhNmfeJMJzpf5E7PquGspT921RmFmks5sSH_cgaJpZM4Ohk-Z .

[jad-hamza]

For the congruence that means we're checking congruence only for the context: let x = HOLE in F and not other type of expression. For instance, not for the context, Lambda(x, HOLE).

[samarion]

Well, it depends: if your HOLE can only be filled by a value, then congruence holds for arbitrary context. If your HOLE can be filled by an arbitrary term (although this doesn't make much sense in the context to call-by-value evaluation), then congruence only holds for the first context.

On Thu, Jul 27, 2017 at 2:33 PM, Jad notifications@github.com wrote:

For the congruence that means we're checking congruence only for the context: let x = HOLE in F and not other type of expression. For instance, not for the context, Lambda(x, HOLE).

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/62#issuecomment-318348649, or mute the thread https://github.com/notifications/unsubscribe-auth/ADKzhBt7z7IY6_1DJZis8O3T1OdpNEZiks5sSIOegaJpZM4Ohk-Z .

[jad-hamza]

Yes, agreed! Though I think there are definitions of equality that do satisfy the more general requirement, even with call-by-value evaluation.

we would still have the same problems for functions that use the argument x.

Personally, I don't know which definition of equality we should use. It's just that this particular definition seems strange/arbitrary to me, because it is the only (?) operation that inspects the structure of the expression. Also, it is not consistent with function extensionality and general congruence/substitution. I think it's fine to have a definition of equality that does not always imply function extensionality (weaker), but a definition which contradicts it seems odd.

In general, I also think it's ok if we have a definition of equality that is not decidable/computable. The RecursiveEvaluator is already a partial function (e.g. due to recursion and quantifiers).

If the evaluator fails to check for equality, then it can hang or return UNKNOWN (like it does for non-terminating function and for some quantifiers). Of course the evaluator would never hang for equality on base types (if the evaluation terminates), because equality here is decidable. The evaluator could even use the current implementation, and return UNKNOWN if it's not able to prove equality using the current definition (nor disprove).

[samarion]

I believe that consistency with extensionality and general congruence/substitution are not so useful properties in the context of a program verifier. I think that having the ability to evaluate programs under models and consistency with clear operational semantics are more important. In this sense, uncomputable definitions are really bad! Currently, only quantifiers (and choose, which you can view as a quantifier) have this unfortunate property and I'd like to avoid introducing it anywhere else.

About contradicting extensionality, there is no way to avoid this while ensuring that equality both 1) is computable for all values, and 2) terminates and returns either true or false. If we relax either of these requirements, then there are many other useful and interesting notions that become available, but I believe these are useful properties for verifying Scala code. Also, although the notion seems a little arbitrary, it is computable and satisfies general congruence for value substitutions, thus making it rather attractive in the context of both program evaluation and verification.

Finally, if you want to use a different notion of equality, it is fairly easy to encode these into the Inox fragment using either the HasADTEquality() flag or implicit capabilities in the frontend. On the Stainless side, this would look something like:

1. Extensional equality:

case class ~>[F,T](f: F => T) { def apply(arg: F): T = f(arg) override def equals(that: Any): Boolean = that match { case f2: ~>[F,T] => forall((arg: F) => f(arg) == f2.f(arg)) case _ => false } }

2. Equality with capabilities:

case class Eq[T] { def apply(t1: T, t2: T): Boolean }

def equals[T](t1: T, t2: T)(implicit cap: Eq[T]): Boolean = cap(t1, t2)

3. Equality with unknown: generate all relevant equality functions on the Stainless side and provide interface @ignore implicit class ThreeValuedEquals[T](val e: T) { def ===(that: T): Option[Boolean] = sys.error("Should be implemented within Stainless") }

Note that extraction for options 1 and 2 is not quite available yet in Stainless but support is ready on the Inox side.

On Thu, Jul 27, 2017 at 2:52 PM, Jad notifications@github.com wrote:

Yes, agreed! Though I think there are definitions of equality that do satisfy the more general requirement, even with call-by-value evaluation.

we would still have the same problems for functions that use the argument x.

Personally, I don't know which definition of equality we should use. It's just that this particular definition seems strange/arbitrary to me, because it is the only (?) operation that inspects the structure of the expression. Also, it is not consistent with function extensionality and general congruence/substitution. I think it's fine to have a definition of equality that does not always imply function extensionality (weaker), but a definition which contradicts it seems odd.

In general, I also think it's ok if we have a definition of equality that is not decidable/computable. The RecursiveEvaluator is already a partial function (e.g. due to recursion and quantifiers).

If the evaluator fails to check for equality, then it can hang or return UNKNOWN (like it does for non-terminating function and for some quantifiers). Of course the evaluator would never hang for equality on base types (if the evaluation terminates), because equality here is decidable. The evaluator could even use the current implementation, and return UNKNOWN if it's not able to prove equality using the current definition (nor disprove).

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/epfl-lara/stainless/issues/62#issuecomment-318352749, or mute the thread https://github.com/notifications/unsubscribe-auth/ADKzhKTcxdG-pfKxfAB1qAOs8aMskwBdks5sSIgSgaJpZM4Ohk-Z .

[jad-hamza]

Alright, thanks for all the explanations!