MeTTa should support single sided matching
Opened this issue · 17 comments
Describe the bug
I believe MeTTa should seamlessly offer single sided matching alongside double sided matching. In the sense that the developer should be able to easily specify when reduction should take place, under which conditions, in this case single sided matching.
To Reproduce
Single sided matching is the default in traditional functional programming languages, that should be enough of a reason. Let me nonetheless describe a situation where it is useful. For instance, the following SKI combinaroty logic reduction rule is only correct if MeTTa reduction is single sided
(= ((S K) K) I)
Expected behavior
Try for instance
!((S K) $x)
With single sided MeTTa reduction, it should remain unreduced.
Actual behavior
It reduces to
[I]
which is incorrect according to SKI combinator logic.
Additional context
I tried to work around that by adding the following type definitions
(: (S K) (-> Symbol $a))
which did not work.
I also tried
(: K Combinator)
(: (S K) (-> Combinator $a))
which did not work either, though this is not surprising since Combinator is not a meta type.
Also, these workarounds would not address the broader issue of doing only singled sided reduction on demand.
I also tried to write my own reduction function using case but since case is double sided, it is not directly possible either. The only alternative I found is to deconstruct the term and use == here and there to identify the pattern, which sorta defeats the point of having a language based on pattern matching.
For instance, for that specific example, the code would be
(= (reduce $term) (if (== $term ((S K) K)) I (empty)))
which is still OK since the pattern to identify is constant, but it becomes far less elegant when the reduction rules involve more sophisticated patterns such as
(= (((S $x) $y) $z) (($x $z) ($y $z)))
Also, I think this falls under the broader issue of controlling when and when not to reduce, such as reducing or not reducing the first variable of an expression with a function, such as discussed in issues #642 or #242, or reducing till bindings are ready #659.
As a few quick remarks:
Single sided matching is the default in traditional functional programming languages, that should be enough of a reason.
I disagree with this reason, because traditional FPLs simply don't support constructions like ((S K) $x).
which is incorrect according to SKI combinator logic.
I also disagree that this is incorrect. Reducing ((S K) $x) to I is precisely correct in accordance to MeTTa semantics. The following program
(= ((S K) K) I)
!(the result of (quote ((S K) $x)) is ((S K) $x))
produces [(the result of (quote ((S K) K)) is I)], which makes perfect sense to me.
Apparently, we don't want to change this behavior. In general. I don't see from the "bug description" what the issue really is. I can guess that in some cases we may want to work with expressions with variables as is, avoiding substitution of variables, and we may need to come up with some idiomatic way of doing so. But it would help, if you describe, what you are trying to achieve in your use case.
I mean, maybe, you can use something like ((S K) (Var $x)) in your use case, I don't know. MeTTa is symbolically very low-level, and when you need to distinguish two things, you may need just to add custom symbols to distinguish them, and add rules for processing two different situations. If we want to say that we want to reduce something or not, we will need to have some syntax for these two options anyway, right? Maybe, it can be done by custom symbols in MeTTa itself rather than by adding some built-in means to the interpreter. So, please, explain your use case in more detail
I would agree that something like (: (S K) (-> Symbol $a)) or (: S (-> Symbol (-> Symbol $a))) could prevent ((S $x) $y) from reduction. But this is the same issue as #673 .
Reducing ((S K) $x) to I is precisely correct in accordance to MeTTa semantics.
I agree.
So, please, explain your use case in more detail.
My use case is to emulate lambda calculus and combinatory logic in MeTTa, and, ideally, to do that elegantly. The solution I have so far is not elegant, I guess that's my issue, other than that it works so it's not that bad.
See https://github.com/ngeiswei/hyperon-chaining/blob/23ac2aad8671a19fc6234b9679468fcd429ca977/experimental/hol/calculi-converter.metta#L464-L627 for my solution so far.
If I had a one-sided case construct, I think it would solve my problem. Do you think such one-sided case can be implemented in pure MeTTa?
But there is a deeper issue: is two-sided reduction too unconstrained to be the default?
Two-sided reduction is forcing us to deal with annoying corner cases such as when a variable matches a function as in issues #642 or #242. I wonder whether these issues are not the manifestation of a bigger problem, which is that two-sided reduction, as a default spontaneous reduction behavior, is too unconstrained.
I understand that inference control could potentially come to the rescue to constrain reduction, and maybe that's a valid solution (it should then also be a solution for emulating combinatory logic and lambda calculus). Still, I wonder...
I looked at the example you provided and I believe the issue is that when a combinator expression is generated from lambda expression and something like ((S K) $x) is generated then it is incorrectly reduced to I. Is it correct?
I am not 100% sure (because I didn't fully read the code) but is it possible using ((S K) (Var x)) (similarly to ((S K) (Var $x)) suggested by Alexey) where Var is a "custom variable" prefix to build what you want?
Saying this I don't fully deny the idea of a single side matching. For instance single-side eval could be an optimization in a code where programmer knows in advance that double-side matching is superfluous.
is it possible using ((S K) (Var x)) (similarly to ((S K) (Var $x)) suggested by Alexey) where Var is a "custom variable" prefix to build what you want?
It should be possible, although I would prefer a more elegant alternative if there is one. But maybe that's the best.
Saying this I don't fully deny the idea of a single side matching. For instance single-side eval could be an optimization in a code where programmer knows in advance that double-side matching is superfluous.
Maybe what could be useful is to have a single-side match built-in operator (called say single-side-match or any other better name). Then given that the developer should be able to reimplement in pure MeTTa single-side case, single-side let, etc, and ultimately single-side reduction.
The number of cases where single-sided matching evaluation would be useful is adding up. Here they are
- MOSES reduction rule. A reduction rule is not supposed to add structure to a term, therefore single-sided matching evaluation is required.
- Backward Chaining inference control. Single-sided matching evaluation could be used to prune the search space by avoid adding expensive proof constructs, yet keeping the ability to verify them where there were already there.
One can write MeTTa code that works around the lack of single-sided matching evaluation, using case, if and ==, but the resulting code is not pretty. It is sad that in those situations the MeTTa code is less elegant that its FP counterpart.
I don't know exactly what is the correct way to remedy that. Ideally the programmer should have the ability to decide at each function entry point, whether it should be double or single sided evaluated. Let me give an example. Assume foo has two entry points, one which is double-sided, and another one which is single-sided.
(= (foo (A $x)) (B $x)) ; Double-sided matching
(= (foo (C $x)) (D $x)) ; Desideratum: single-sided matching
So the following call
!(foo $x)
would only return
[(B $x#1)]
instead of
[(B $x#1), (D $x#2)]
As (foo (C $x)) being single-sided, only
!(foo (C $x))
would trigger that entry point, and return [$x].
I believe that is the level of control we want. How to represent that control? I don't have a clear answer. I suppose one place could be the type signature, but it would only work if one can associate a type to, not just a function, but a function entry point. Thus requiring inline type definitions.
Any idea?
Perhaps a good way would be in the = symbol. For instance
(=^ (foo (C $x)) (D $x))
would be singled-sided evaluated.
I wonder what combination would convey the idea of single sided. I can think of
=.=|=>
An other alternative is to make single-sided the default, and have a new equality for double-sided, such as <=>, or such. The pros of having single-sided as default is that it is less disorienting for the new programmers. The cons is, if double-sided evaluation is more frequent in MeTTa programs, then it is further away from an optimal Shannon encoding.
I'd like to provide yet another example where single-sided evaluation would be useful. The following MeTTa code
;; Reduction rule for symmetry
(= (: (Sym (: (Sym (: $x $a)) $b)) $c) (: $x $a))
;; Test reduction
!(: (Sym (: (Sym (: $x $a)) $b)) $c)
enters an infinite recursion. If I could define such reduction rule as a single-sided matching, then it would output the correct result, which is (: $x $a).
Why do I need such reduction rule, you may ask? Sym is a proof constructor such that given a proof of x = y, builds a proof of y = x. Obviously
(Sym (Sym PROOF))
is equivalent to PROOF. The rule provided above simply expresses that, but works on a fully type-annotated term.
As we discussed at MeTTa Study Call, this
MeTTa should seamlessly offer single sided matching alongside double sided matching
can be understood differently. One may write a pretty simple grounded function, which replaces all variables in the expression to be evaluated with placeholders like $x -> (ScreenOut x), perform unification, and then make backward replacement. This can be easily added as an experimental feature (will it provide a single-sided matching?). This the present issue is a blocker, then it is way to go. However, the phrase "MeTTa should seamlessly offer" may suppose that this operation should be a part of core semantics, or there should be a way to implement it in pure MeTTa.
But if we think about implementing this feature in the current MeTTa (either via grounded functions or pure MeTTa, but with the use of unification), the drawback is that we implement a simpler operation by reusing a more complex operation, which is not be the most efficient way. Thus, the question is whether the issue supposes that one-sided pattern matching should be the core operation with its own implementation (and either unification should rely on it, or there should be two different implementations). Thus, I wonder
@vsbogd , if the current implementation of unification relies on one-sided pattern matching, which can be exposed to MeTTa?
@ngeiswei , what exactly do you mean by "MeTTa should seamlessly offer single sided matching alongside double sided matching" (in the context of the above comment)?
if the current implementation of unification relies on one-sided pattern matching, which can be exposed to MeTTa?
I would say it is pretty easy to implement single-sided matching as a separate function inside core library. Current double-side matching implementation basically uses the Bindings data structure and calls its methods using variables from both matched atoms. We could rewrite high level function (which is small code snippet) to the single-side matching.
To me the main question is how to embed this implementation into language naturally.
the question is whether the issue supposes that one-sided pattern matching should be the core operation with its own implementation (and either unification should rely on it, or there should be two different implementations).
I don't know if double-sided unification can be easily derived from single-sided unification. It seems to me they kinda both derive from a more general, more controlled unification. I suppose they mostly differ by the substitution step, double-sided operates substitution over all variables while single-sided operates substitution over variables on one side only.
So, maybe if we split unification into two steps
- unification per se
- substitution
and expose these two steps to MeTTa, then the user can have fuller control over the whole thing, including choosing between "double-sided vs single sided" unification.
@ngeiswei , what exactly do you mean by "MeTTa should seamlessly offer single sided matching alongside double sided matching" (in the context of the above comment)?
My belief is that there is a utility in having single-sided unification across all functions that rely on unification, match, let, case, function call, maybe more. So by seamlessly, I suppose I mean that MeTTa would offer constructs to do both. Of course, depending what primitives are available, some constructs could merely be functions in the standard library.
To me the main question is how to embed this implementation into language naturally.
I was thinking of some character, either indicating single-sided if double-sided is the default, or indicating double-sided if single-sided is the default. For instance
| single-sided | double-sided |
|---|---|
| match% | match |
| case% | case |
| let% | let |
| let*% | let* |
| unify% | unify |
| =% | = |
I suppose they mostly differ by the substitution step
Actually, that is not true, so the functionality is a little more complicated to break apart.