MeTTa should support single sided matching

[ngeiswei]

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 https://github.com/trueagi-io/hyperon-experimental/issues/642 or https://github.com/trueagi-io/hyperon-experimental/issues/242, or reducing till bindings are ready https://github.com/trueagi-io/hyperon-experimental/issues/659.

[Necr0x0Der]

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.

[Necr0x0Der]

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

[Necr0x0Der]

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 .

[ngeiswei]

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?

[ngeiswei]

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 https://github.com/trueagi-io/hyperon-experimental/issues/642 or https://github.com/trueagi-io/hyperon-experimental/issues/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...

[vsbogd]

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?

[vsbogd]

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.

[ngeiswei]

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.