-
Notifications
You must be signed in to change notification settings - Fork 54
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
Strange behavior of lambda equality #62
Comments
I'll have to take a look at what imperative is doing here. I can also take a look at #30 while I'm at it. About equality, we can't say that 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. |
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 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)? 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 |
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 ***@***.***> 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
<#62 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ADKzhAFXDbiSywN9ETaBQkjgd7RfGHlKks5sRdkWgaJpZM4Ohk-Z>
.
|
If I understand correctly, all threes variants are invalid for the operational semantics of Inox (and valid if we replace |
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
```scala
val v = plus(Zero(), Zero())
(x: Nat) => u == (x: Nat) => v
```
…On Tue, Jul 25, 2017 at 2:59 PM, Jad ***@***.***> 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
<#62 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ADKzhLGHIz1Mqa9r_2UQGVnRN_9l7DKSks5sRea8gaJpZM4Ohk-Z>
.
|
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? epfl-lara/inox#31 I wonder if removing that case breaks anything else? |
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 ***@***.***> wrote:
Hmm I see, that's funny
By the way, is this the code responsible for the strange behavior?
epfl-lara/inox#31 <epfl-lara/inox#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
<#62 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ADKzhE8Yi3_cNMjFiJVX9faQncbQdFXlks5sRezmgaJpZM4Ohk-Z>
.
|
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 (In the examples above, x is u, and t is plus(Zero,Zero)) |
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 ***@***.***> 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
<#62 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ADKzhDt2mTHt_z1_eurdka8Fxo_4Enmcks5sRfEogaJpZM4Ohk-Z>
.
|
Fixed by epfl-lara/inox#31 |
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 |
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 ***@***.***> 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
<#62 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ADKzhO01bKW9EBUODgjsr9-WRpUckvofks5sSFS_gaJpZM4Ohk-Z>
.
|
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 If I understand correctly, for Inox, this judgement is defined in terms of the operations semantics in RecursiveEvaluator. More precisely, we have Evaluating a forall requires a similar definition right? The expression forall((x: T) => e) evaluates to true if |
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))
}
} |
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 ***@***.***> 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
<#62 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ADKzhGSN5C96SLzUecJPa4sG3tozNP-jks5sSHT3gaJpZM4Ohk-Z>
.
|
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 <[email protected]>
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 ***@***.***> 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
> <#62 (comment)>,
> or mute the thread
> <https://github.com/notifications/unsubscribe-auth/ADKzhGSN5C96SLzUecJPa4sG3tozNP-jks5sSHT3gaJpZM4Ohk-Z>
> .
>
|
Can you expand a bit on the definition of congruence you have in mind? So do we want I thought the Sigma would be populated when entering in a let binding? (Would that be the context rctx: RC in the RecursiveEvaluator?) |
Equality is defined on "Expr", so for congruence I had in mind this:
|
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)? |
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 ***@***.***> 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
<#62 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ADKzhNmfeJMJzpf5E7PquGspT921RmFmks5sSH_cgaJpZM4Ohk-Z>
.
|
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). |
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 ***@***.***> 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
<#62 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ADKzhBt7z7IY6_1DJZis8O3T1OdpNEZiks5sSIOegaJpZM4Ohk-Z>
.
|
Yes, agreed! Though I think there are definitions of equality that do satisfy the more general requirement, even with call-by-value evaluation.
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). |
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 ***@***.***> 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
<#62 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ADKzhKTcxdG-pfKxfAB1qAOs8aMskwBdks5sSIgSgaJpZM4Ohk-Z>
.
|
Alright, thanks for all the explanations! |
f1
andf2
should be equal here. It looks like that the imperative cleanup transformation replacesplus(Zero(), Zero())
byu
inf2
. For Stainless,u
andplus(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?Result after transformation by imperative.cleanup, probably due to the call to
simplifyLets
.The text was updated successfully, but these errors were encountered: