Open noskill opened 9 months ago
Rust MeTTa and Minimal MeTTa have different implementations for add
. The first one implements and
as a grounded operation. The problem with grounded operations is that they require interpreting their arguments before running the operation itself unless the operation arguments are of Atom
type. However, in the latter case, it is not possible right now to declare that the argument type is Bool
also. The same problem arises for and2
implementation. Minimal MeTTa implementation for and
is in MeTTa itself, so it could be replaced in principle, but the type signature looks not too nice.
As a side remark, there is a question in semantics. In constructive mathematics, something can be provable, refutable, and undecidable. If the process never stops, its result is neither true or false. The question is how we define and
in this case. and
can be false if one of the arguments is provably false, or it can be true if both arguments are provably true. But this would be better to define in terms of dependent types.
In any case, what I don't like in such and2
is that it is not symmetric. That is, (and2 (loop) False)
will not terminate. I know that many traditional programming languages have this special semantics for and
. But I'd say that and
is not that special, and the problem boils down to the order of computations, which we'd like to control. It might be perfectly ok for and
to evaluate both operands, and if someone wants to avoid this, it should be done explicitly. We are lacking this feature atm, but there can also be different ways to introduce it. Maybe, some form of lazy computations could provide one approach. But maybe, we need to address this via parallel and sequential composition operations. With such operations, we could describe two different and
s. In a sequential and
, we would explicitly indicate that the first argument is calculated before the second. Parallel and
could calculate both arguments simultaneously and terminate, when one of them returns False
or both of them return True
.
This can be considered as a possible future extension of Minimal MeTTa or as a feature of rholang space.
I agree that a function that gets stuck in a loop does not return a boolean, but that is not the point. What we usually have is some long-running function that will return a boolean but will run too long. Also i agree that might be better solutions like adding concurrent execution or iterative deepening execution strategy like in ciao prolog https://ciao-lang.org/legacy/files/ciao/ciao-1.5p133/ciao_html/ciao_97.html, it will provide symmetry, at least if we don't pass there some grounded function. Or maybe gounded functions should be called in a separate thread, while metta interpreter will continue it's execution in the main thread?
Anyway sequential and is a sensible default, better than the current implementation. Current implementation is symmetrical but why it is an advantage?
This program will stick in the loop:
Evaluating the second argument will harm the performance even if the second argument doesn't contain infinite loop
instead we can rewrite and via if
this and will return False