Incorrect result on some inputs

[Ekdohibs]

HVM produces incorrect results on some inputs, one of which being:

(Main arg) = ((λa (a (λb ((λc (λd (b (c d)))) a)))) (λe (e e)))

On this input, HVM produces the result λx1 λx2 ((x1 x2) (x1 x2)) while the correct result is λx1 λx2 ((x1 x1) (x2 x2)) (as verified by [https://crypto.stanford.edu/~blynn/lambda/](), with the corresponding input syntax by adding dots after the variable of each lambda: ((λa. (a (λb. ((λc. (λd. (b (c d)))) a)))) (λe. (e e)))).

Besides, on other inputs such as:

((λa λb ((b a) λc λd (λe (d a) a)) λf (f f)) λz z)

HVM produces the result λx1 (x1 λx2 (x2 _)) which is not even well-formed.

[VictorTaelin]

This seems to be violating the "clones can't clone their own clones" limitation, explained here. HVM is just a (much) faster functional runtime based on the abstract algorithm, not a full λ-calculator. Attempting to make a clone clone its own clone is considered undefined behavior. I stress that this only happens in highly artificial examples (like these!).

Edit: I now consider HVM should be seen as an Interaction Net runtime that happens to be a suitable as a functional back-end, as long as compatibility is ensured by a type-checker or something equivalent. But there is no such a thing as UB, as these reductions are correct w.r.t. INet semantics. See below for more info.

[L-as]

This limitation should probably be noted in the README. You probably also want to add more information on the limitation to make clear under what situations this is (im)possible. I assume this limitation is impossible to hit if the type system precludes applying a function to itself?

[Ekdohibs]

While I agree it is ok if there are limitations, I find it a completely different matter to have limitations and to silently return an incorrect result! Besides, it seems to me that this limitation could be easily violated in a "natural" program such as mapping over a list of lists: map2 f l = map (map f) l. The function map has to clone the function given to it (as it needs to call it several times), but map f contains a clone of map itself!

[VictorTaelin]

@L-as yes, but that is still too restrictive. Applying a function to itself is fine (and even usual). For example, the Y-Combinator relies on applying r to itself: Y = λf (λr(f (r r)) λr(f (r r))). That is completely fine. What is not allowed is for a cloned function to apply its own clone to itself. That is a much more rare situation. I'd bet there isn't a single occurrence of this in any of the Rust's top 1000 libraries, for example. There could be a note on the README, but is it really necessary. This, again, is way less restrictive than Rust's borrow checker, so I find it really confusing that people make a big deal of this.

[VictorTaelin]

@Ekdohibs map (map f) l is completely fine! As is basically anything you'll come up with in practice. I think this is the main reason people get scared, they don't realize what the limitation really entails!

As to silently failing, that's just like every other undefined behavior, not unlike adding a number and a string, or reading arrays out of bounds. HVM is an untyped compile target, not meant to be a user-facing language. Obviously languages that compile to it will prevent these programs during type checking.

[Ekdohibs]

Hmmm, I think I don't understand why map (map f) l is fine, at least if map is a lambda-bound function. (Imagine we are in Haskell and this function map2 is defined for any functor).

[nothingnesses]

Victor gave an example of what isn't allowed on the Telegram channel:

let f = λs. λz. (s (s z)) # a lambda that clones its argument
let g = f                 # a clone of that lambda
(g f)                     # the clone will clone the original

He said:

this is a limitation of the runtime and should raise a type error, just like you can't have two concurrent &mut references in Rust

[VictorTaelin]

I think people (myself included!) misread the meaning of "a clone cloning its own clone". The map function just creates copies of f. Then the outer map creates copies of map f. There is no cloned function attempting to clone itself. That would happen, perhaps, if Map called (f f), and was applied to a function that called its argument on itself. Like this:

(Map f Nil) = Nil
(Map f (Cons x xs)) = (Map ((f f) x) xs)

(Main) = (Map λx(x x) (Cons 1 (Cons 2 (Cons 3 Nil)))))

But that's not the definition of map. Even if that was the definition of map... most mapped functions are linear (like λx(+ x 1)). And even if the mapped function wasn't linear, it would probably not be calling its input on itself. Do you see how far your example is from reaching the limit? The program above doesn't even make sense. It is difficult to even come up with well-typed examples that reach this limitation. Church Nat is the only one I know, actually. And if once in a blue moon an user happens to reach this limitation, fine; just let the clone-of-clone-checker show him/her a type error (on the input language, not HVM). Should be an easy fix. Rust shows us 50 borrow-checker complaints every time we compile anything, and everyone is fine!

[Ekdohibs]

Ah, I thought creating copies of map f would create copies of map, but I guess I'm mistaken about it. I've seen more than once your example above of writing the double function and calling it on itself, but it was mainly to test that compilers were correct. I'm still not sure about the precise conditions of "a clone cloning its own clone". Supposing f clones its argument, f f is not allowed. However, is f 0 f allowed if f clones its second argument? Is f (\x. f x) allowed? What about f (f g) and f (g f) depending on g? In any case, it seems non-obvious to me to come with a type system to forbid such clones, and I fear such a type system might be as difficult to understand as Rust's borrow checker...

EDIT: actually, I think I don't even understand why the Y combinator would be fine. r is applied to (a clone of) itself, which is fine for the first step of reduction. However, for the second step, the two occurences of r are both clones of the rightmost lambda-term. Applying r to itself then is a violation of the "clone cloning its own clone" rule, I would have thought?

[VictorTaelin]

@Ekdohibs think about it like this:

1. Every duplicator on the source (dup x y = term) has a unique label.

2. A duplicator can't copy a term that has a duplicator with the same label as itself.

For example:

(λf(dup#0 x y = f; (x y)) λg(dup#1 a b = g; (a b)))
---------------------------------------------------
dup#0 x y = λg(dup#1 a b = g; (a b)); (x y)
---------------------------------------------------
(λg(dup#1 a b = g; (a b)) λg(dup#1 a b = g; (a b)))
---------------------------------------------------
dup#1 a b = λg(dup#1 a b = g; (a b)); (a b)

The last line is undefined behavior, because it has a dup with a #1 label attempting to copy a function which has a dup with a #1 label. Notice that the first level of self-copying is fine. It is when clones clone clones that you get a problem.

This can only happen when a function copies itself, and then the copy also copies itself. Emphasis on the "self". Functions copying other functions is fine. Repeated self-copying is the only way, because, otherwise, it would be impossible for two identical labels to collide, since every dup has a globally unique label.

In general, any program that isn't allowed is similar to (λx(x x) λx(x x)) in shape. For example, the first program you posted is just a larger version of it:

(Main arg) = ((λa (a (λb ((λc (λd (b (c d)))) a)))) (λe (e e)))
(Main arg) = ((λa (a ........................ a..)) (λe (e e)))

And the second one expands to it after a few steps.

It is not hard to come up with a static checker for this requirement. For example, the old Formality-Core had one, but it was too restrictive, because it stratified programs in levels, so that a dup on level X could only copy terms on level X+1, avoiding this problem. A much better solution, I believe, would be to just track a function's lifecycle and make sure it isn't cloning itself, followed by its clones also cloning themselves.

[Ekdohibs]

Ah, that makes it clearer, thank you! However, with this definition, I still think the Y-combinator will be undefined behavior.

[VictorTaelin]

No, because the Y-combinator just creates infinite copies of the function it receives, but it never actually copies itself, nor does the function it receives copy itself. But applying the Y-combinator to itself is undefined behavior.

I understand your point that it might be annoying to demand such a checker for any language interested to compile to HVM, though. Perhaps we could provide a checker as part of HVM, somehow. I'll think about that.

[VictorTaelin]

I'll close this issue and link to it on the needed improvements thread, in case anyone is interested in contributing with this in particular.

(@Ekdohibs feel free to re-open if you want to ask more questions!)

[Ekdohibs]

In the Y-combinator case, it is neither the function it receives nor the Y-combinator which copies itself, but the (\r. f (r r)) subterm. If we expand the body of the Y-combinator to (\r. dup#0 s t =r ; f (s t)) (\r. dup#1 s t = r; f (s t)), after a reduction it becomes (\r. dup#1 s t = r; f (s t)) (\r. dup#1 s t = r; f (s t)), and the dup#1 needs to copy a dup#1.

[Ekdohibs]

@VictorTaelin (it seems like I can't reopen the issue, since you were the one to close it, however).

[VictorTaelin]

Ah, that is a fair point, a sub-term of the Y-combinator does clone itself, and then that clone clones itself again. That should be undefined behavior according to my explanation, so you're right. What happens, though, is that the duplication process is never finished, because (r r) gets pushed infinitely down the recursion, so it actually works fine. The Y-Combinator is a pretty peculiar term. It even has a normal form:

dup#1 s t = r; 
dup#1 S T = R;
(λr(f (s t)) λR(f (S T)))
-------------------------
dup#1 s t = λR(f (S T)); 
dup#1 S T = R;
(f (s t))
-------------------------
dup#1 s t = (f (S T)); 
dup#1 S T = #1{R0 R1};
(f (λR0(s) λR1(t)))
-------------------------
dup#1 s t = (f (S T)); 
dup#1 S T = #1{λR1(t) R1};
(f s)
-------------------------
dup#1 s t = (f (λR1(t) R1)); 
(f s)
-------------------------
dup#1 s t = (f t); 
(f s)

Note that this "normal form" represents (f (f (f (f (f ....))))). Anyway, you're right, a complete criteria for acceptance would be a little complex. But the description I provided gives us a fairly reasonable language already, I think. A "clone checker" doesn't need to cover all programs that don't produce undefined behavior, it just must result in a practical language. It is a similar situation with Rust: there are many correct programs that the borrow checker simply can't identify as such. A clone checker would perhaps be a whitelist of patterns which we know to be safe.

[Ekdohibs]

I agree, the Y-combinator works correctly, even if it is undefined behaviour. In fact, what I think happens is that we get a duplication confusion (which often produces errors), but here instead, since the Y-combinator has a rather peculiar form, gives us the correct result, albeit with a term containing loops(!). I also found a slightly unsual example, but one that you could see in a real program that should cause a clone error: imagine you have a list of functions, and you want to map each of these functions over a list (that could happen with a list monad for instance). You would have a term of the form map (\f. map f values) functions, and if I'm not mistaken, in this case, map will duplicate its argument, which contains itself a clone of map that will be duplicated (the difference with before being that since the function is statically unknown, the duplication will wait for each call of the function, thus keeping an unreduced dup).

[L-as]

@VictorTaelin When would you ever apply a function to itself in a standard functional language like Haskell or OCaml?

[VictorTaelin]

I don't think that case is problematic, but I can try later.

@L-as applying a function to itself is not that rare. I can think of Church-Nats, and the Y-Combinator. Having to do that once again with the result is quite rare.

[Heimdell]

Well, this should be checked somehow. Which rules do you think are necessary to add to typechecker to catch it?

Should the (f f) application simply emit linearity for the lambda that bounds f?

[Ekdohibs]

With the following code I get incorrect results (as expected):

(Map Nil f) = Nil
(Map (Cons x xs) f) = (Cons (f x) (Map xs f))

(Main arg) =
  let l1 = (Cons (λx(x)) (Cons (λx(+ x 2)) Nil))
  let l2 = (Cons 0 (Cons 1 Nil))
  (Map l1 (λf(Map l2 f)))

The result given by HVM is (Cons (Cons 0 (Cons 3 (Nil))) (Cons (Cons 0 (Cons 3 (Nil))) (Nil))) while (Cons (Cons 0 (Cons 1 (Nil))) (Cons (Cons 2 (Cons 3 (Nil))) (Nil))) is expected and is what we get if we replace an instance of Map by an identical copy.

However, I (personally) find this code to be very reasonable: no self-application, only the classic "Map" function is used, and the most unusual part is arguably the list of functions (which is not even that unusual).

[VictorTaelin]

@Ekdohibs the abstract algorithm handles your program fine, it doesn't hit "the limit". It hits it on HVM due to a temporary peculiarity: HVM currently does not assign different labels to different uses of the same global function. That will be patched soon, and your program will work. As a temporary fix, you could just have two map functions:

(Map0 Nil         f) = Nil
(Map0 (Cons x xs) f) = (Cons (f x) (Map0 xs f))

(Map1 Nil         f) = Nil
(Map1 (Cons x xs) f) = (Cons (f x) (Map1 xs f))

(Main arg) =
  let l1 = (Cons (λx(x)) (Cons (λx(+ x 2)) Nil))
  let l2 = (Cons 0 (Cons 1 Nil))
  (Map0 l1 (λf(Map1 l2 f)))

But again, that's not necessary, since it will be patched soon. I'll notify this issue when that happens.

To be more specific, these lines on compiler.rs will just assign labels defined at compile time to a global function's dup nodes. Instead, we should dynamically generate fresh labels. The only issue with that is that the space for labels is small (2 ** 16), because we use 8 bits for the atomic_flag synchronization operation. This would be easily exhausted if we generate new labels dynamically. So we either need to change the atomic_flag to use 1 bit, or avoid generating the same labels by some external mean, or just increase the space for it, perhaps storing it separately.

[Ekdohibs]

While i completely agree that this fixes the issue (which is what I meant by "replacing one instance by an indentical function" above), this would not work if Map was a function argument instead of a global function (think functors and monads for instance: in the case of monads, This very function, of type Monad m => m (a -> b) -> m a -> m b exists in Haskell and is the well-known and very used function <*>!).

[VictorTaelin]

@Ekdohibs I don't think that is true. Even if Map was built locally with Fix, the Fix function itself would give it brand new labels every time it is generated; right? Or what else you have in mind?

[Ekdohibs]

What I had in mind was a function whose body was the expression above that took Map as an argument, sorry for the confusion.

[L-as]

In Haskell the code might be

x :: Applicative m => m [[Int]]
x =
  let l1 = ((\x -> x) : (\x -> x + 2) : []) in
  let l2 = (0 : 1 : []) in
  pure $ pure (\f -> pure f <*> l2) <*> l1

While not entirely natural, it goes to show that completely legal Haskell exists, while not being valid in HVM.

Unfortunately I don't think HVM will be usable for Haskell unless all legal Haskell is covered, or at the very least a large subset that tells you when you step outside it.

[L-as]

I just realised that my code accidentally uses the Applicative for lists.

The following is perhaps a better example:

x :: (forall a b. (a -> b) -> [a] -> [b]) -> [[Int]]
x mymap =
  let l1 = ((\x -> x) : (\x -> x + 2) : []) in
  let l2 = (0 : 1 : []) in
  mymap (\f -> mymap f l2) l1

[Ekdohibs]

The code I had in mind was something like:

f :: Monad m -> m (a -> b) -> m a -> m b
f x1 x2 = join $ fmap (\f -> fmap f x2) x1

x = f ((\x -> x) : (\x -> x+ 2) : []) (0 : 1 : [])

Notice how the Monad m in the definition of f has a side-effect that the fmap is passed as an argument once typeclasses are lowered, so that the function f makes two clones and applies one to the other.

[phischu]

I just want to say that apparently the original issue has been fixed. The following program:

(Map Nil f) = Nil
(Map (Cons x xs) f) = (Cons (f x) (Map xs f))

(Main arg) =
  let l1 = (Cons (λx(x)) (Cons (λx(+ x 2)) Nil))
  let l2 = (Cons 0 (Cons 1 Nil))
  (Map l1 (λf(Map l2 f)))

Evaluates to

(Cons (Cons 0 (Cons 1 (Nil))) (Cons (Cons 2 (Cons 3 (Nil))) (Nil)))

Moreover, the following program (which I conjecture has been working correctly all the time):

(Map Nil f) = Nil
(Map (Cons x xs) f) = (Cons (f x) (Map xs f))

(Mapping mymap) =
  let l1 = (Cons (λx(x)) (Cons (λx(+ x 2)) Nil))
  let l2 = (Cons 0 (Cons 1 Nil))
  (mymap l1 (λf(mymap l2 f)))

(Main arg) =
  (Mapping (λlλf(Map l f)))

Evaluates to:

(Cons (Cons 0 (Cons 1 (Nil))) (Cons (Cons 2 (Cons 3 (Nil))) (Nil)))

As a meta remark, I am completely with Victor here as I do not understand why this whole thing is so important to some people. It really is a very very obscure corner case that untyped lambda calculus unfortunately has.

[L-as]

The issue is that HVM is fundamentally unusable for most functional programming languages unless this is fixed at its root. Supporting the full LC is not a necessity, but when you go from e.g. GHC Core to HVM, there must be a way of detecting whether this GHC Core term can be translated to HVM. It is possible to make a naïve "type checker" for this, but it's very hard to make one that supports a language expressive enough to support common Haskell idioms AFAIK. If you can not guarantee that, then it's not useful in real-world applications. Why would you build a program that maybe works, when hitting the limit is possible with trivial and standard Haskell code?

[eliasvasylenko]

For HVM to be a useful target for existing functional languages like Haskell it is not necessary to remove this limitation. Rather, what is needed is to detect when this limit is (possibly) hit, and then mechanically transform the program into an equivalent one which does not hit this limit. Is such a transformation possible?

[VictorTaelin]

Both are possible! The general solution is:

1. Check if the Haskell program is EAL-typeable.
2. If yes, compile to HVM directly and run.
3. If not, compile to a full λ-calculus DSL on HVM and run.

The full λ-calculus DSL could be, for example, an HVM implementation of Bottom-up β-reduction, or even Haskell's STG. That way, if a Haskell program is incompatible with oracle-free optimal evaluation, it can be reduced via something akin to STG-on-HVM.

The only issue is that EAL is way too restrictive. I'd like to come up with a more general subset which would cover a wider class of Haskell programs.

[tromp]

Could a simple universal lambda expression like [1] be used as a λ-calculus DSL, assuming that this expression is EAL-typeable ? (one would certainly expect lists of booleans to be).

[1] https://tromp.github.io/cl/Binary_lambda_calculus.html#Lambda_encoding

[VictorTaelin]

I'm closing this issue as this should be the user-facing language responsibility to compile compatible terms. Kind-Lang will do so soon, and we'll be providing materials on how to accomplish this to compile any other language to HVM.

[Kesanov]

I think it would be useful to have a "debug" mode, that would throw a descriptive runtime error and halt the execution when this undefined behaviour is encountered.

This might make HVM great compilation target even for untyped languages. It would also simplify debugging for compiler writers or curious tinkerers that just want to play with HVM.

[VictorTaelin]

The thing is, this is not undefined behavior.

Note that HVM is not a Lambda Calculus runtime, but a Symmetric Interaction Calculus runtime. It is a coincidence that 99% of the functional programs and λ-terms you can write in practice can be compiled to a lightweight interaction combinator, but that's just it - a happy coincidence, that allows us to have a functional-looking syntax.

That said, there is no UB in HVM. It will always give you the correct answer, in relation to Symmetric Interaction Calculus semantics, which, in some cases, differ from λ-Calculus semantics. It is a common misconception that HVM will "fail" when it attempts to reduce a λ-term that is deemed "incompatible", but it will not. It will just give a different answer, since the semantics of interaction combinators differ from λ-Calculus semantics regarding the behavior of non-linear variables.

That's why it wouldn't make sense to halt execution even if it was possible to detect such divergent cases (and it isn't). Not everyone comes from a λ-calculus point of view. It is perfectly valid to use HVM as just a raw interaction net runtime.

[LPTK]

If HVM is not a Lambda Calculus runtime, then isn't comparing it with GHC-compiled Haskell, as done on the main page, comparing apples with oranges?

I had the feeling that HVM was advertised as a possible alternative backend for functional programming languages, assuming that some (for now unspecified) type system is added to check that the terms being compiled don't exercise the part where HVM semantics differ (clone that clones itself etc.). Are you now saying that this endeavor is misguided?

it wouldn't make sense to halt execution even if it was possible to detect such divergent cases (and it isn't)

It seems that as long as the divergent case is rigorously specified in terms such as "a clone shouldn't clone itself", it should be possible to check at runtime, even though possibly at great runtime cost. I am curious to hear what it is that makes you think this is in fact impossible.

[jdehaan]

To my understanding computing is computing no matter if the system is using a turing machine approach, interaction nets or lambda calculus, let the most efficient approach (or implementation of it) win. I mean thereby the common level at which things are comparable is the computation efficiency on the same tasks.

[VictorTaelin]

That isn't what I meant. What I said is that divergent terms shouldn't be UB or abort because HVM will give you the correct answer w.r.t Interaction Net semantics, and someone could very well use HVM as an Interaction Net runtime. That isn't mutually exclusive with HVM being a suitable functional runtime. It is a good idea to compile a functional language to HVM, you just need to keep in mind that you need a checker for compatibility, possibly in the shape of an elementary affine type inferencer or something similar.

[LPTK]

Right, so I think you got hung up on @Kesanov's use of "undefined behavior". I think they meant that terms with divergent semantics could be defined as UB from the point of view of a lambda-calculus-based functional language implementation that would compile to HVM. I.e., the compiler would guarantees lambda-calculus semantics within some boundaries, and outside of these boundaries all bets would be off, which is what would allow it to optimize the code (by compiling to HVM).

Now, @Kesanov was not suggesting that HVM crash on divergent programs, but just that it would be useful (for developers of lambda-calculus compilers) to have a debug mode to detect these divergent cases, just like address sanitizers and other instrumentations can detect when a program goes outside of its semantically-specified subset. Do you still think this would be impossible to implement?

[VictorTaelin]

Ah, I see. Sadly, I'm not sure how that could be implemented. After the initial compilation from λ-calculus to interaction nets, the graph will go through intermediate states that don't even correspond to λ-terms. It is not obvious to me how we could identify exactly when a divergence occurs. But I'm not sure if that's not possible either; perhaps there is some easy way to do so. I'll reply here again if I have any additional insight.

[Boscop]

@VictorTaelin What do you think about this?:

An impure solution to the problem of matching fans: https://arxiv.org/abs/1710.07516

(It builds upon this earlier paper: https://arxiv.org/abs/1701.04691)

This solution only requires a (concurrent) hashmap. It's implemented here https://github.com/codedot/lambda and online demo here: https://codedot.github.io/lambda/ E.g. if you enter (g: g g) (s: z: s (s z)), you get the right result v1, v2: v1 (v1 (v1 (v1 v2))). (And if you enter @Ekdohibs's original term as ((a: (a (b: ((c: (d: (b (c d)))) a)))) (e: (e e))), you get the expected result v1, v2: v1 v1 (v2 v2).)

In the benchmarks table, it shows that it reaches the result in fewer interactions than other approaches. Although it fails to reduce the term (f: f (f (x: x))) (i: (f: f (x: x) (f (x: x))) (x: (h, u: h (h u)) (y: x (i y)))) for some reason.

[VictorTaelin]

If my memory doesn't fail me, this paper doesn't prove correctness, and later on Anton found some counter-examples to it, so the solution is wrong. But I could be mistaken about that. The solution is interesting if it works, but a proof would be needed to rely on it.