There is some difference between defining nondeterminism in metta and jetta.
ATM, jetta has a built-in nondeterministic function seq, on top of which custom nondeterministic functions can be defined. This function is absent in metta, but it can be solved on the jetta-wrapper/client side. A more problematic issue is that metta-ish way of defining nondeterministic functions is to define multiple equalities, e.g.
These equalities can be mutually exclusive (resulting in deterministic functions), say
(= (map $f Nil) Nil)
(= (map $f (Cons $x $xs))
(Cons ($f $x) (map $f $xs)))
Multiple equalities are now supported for none of these cases.
Apparently, if we want to compile ordinary metta code, we need to somehow proceed functions defined with multiple equalities.
While the second case is not urgent now since symbolic atoms are not implemented in jetta in any case, we can narrow down this question to the first case, although it may make sense to consider these cases together.
So, how to proceed with the first case (let's suppose that we know that this function is multivalued)? One way is to transform the multiple-equality based function definition into an ordinary functional form with the use of seq, e.g.
(= (bit-1eq $case)
(case $case (
(0 0)
(1 1))))
(= (bit) (bit-1eq (seq 0 1)))
This can be done on the client side, but it would be better to do on the server/compiler side.
This approach may handle (maybe not in the most efficient way and with some complications) any function defined with multiple equalities. But maybe there are other approaches.
@khud , any thoughts?
There is some difference between defining nondeterminism in metta and jetta.
ATM, jetta has a built-in nondeterministic function
seq, on top of which custom nondeterministic functions can be defined. This function is absent in metta, but it can be solved on the jetta-wrapper/client side. A more problematic issue is that metta-ish way of defining nondeterministic functions is to define multiple equalities, e.g.These equalities can be mutually exclusive (resulting in deterministic functions), say
Multiple equalities are now supported for none of these cases.
Apparently, if we want to compile ordinary metta code, we need to somehow proceed functions defined with multiple equalities.
While the second case is not urgent now since symbolic atoms are not implemented in jetta in any case, we can narrow down this question to the first case, although it may make sense to consider these cases together.
So, how to proceed with the first case (let's suppose that we know that this function is
multivalued)? One way is to transform the multiple-equality based function definition into an ordinary functional form with the use ofseq, e.g.This can be done on the client side, but it would be better to do on the server/compiler side.
This approach may handle (maybe not in the most efficient way and with some complications) any function defined with multiple equalities. But maybe there are other approaches.
@khud , any thoughts?