Unifying a structure of variables with a structured function name is not disabled

[ngeiswei]

What is your problem?

Unifying a structure of variables with a structured function name is not disabled by the absence of variable_operation.

How to reproduce your problem?

Run the following code

(= ((W $x) $y) (($x $y) $y))
!(($x $y) $y)

What would you normally expect?

It should end with the output

[(($x $y) $y)]

What do you get instead?

It gets trapped in an infinite recursion.

What else do you have to say?

My assumption is that the absence of variable_operation should cover that case. If not then I need another solution, maybe involving Minimal MeTTa or inference control. To give more context I'm trying to emulate combinatory logic, W is an actual combinator.

The problems occurs in both old and Minimal MeTTa.

[ngeiswei]

Any progress on that? It is somewhat of a blocker.

[vsbogd]

I raised #668 with the fix which prevents from evaluation any expression which has a variable on the first position of the nested expression on the first position. Despite the PR fixes this specific scenario I would say the overall semantics of the evaluation is not clear.

@ngeiswei could you please point to the specific code in https://github.com/trueagi-io/hyperon-pln/pull/44 which is blocked by this issue? I would like to understand which semantics do you need.

[ngeiswei]

The combinatory logic reduction rules

https://github.com/trueagi-io/hyperon-pln/blob/955f0cd1d5839b16abb4e5314cc0f7a602ac8981/metta/hol/calculi-converter.metta#L350-L369

combined with the function that converts combinatory logic to lambda calculus

https://github.com/trueagi-io/hyperon-pln/blob/955f0cd1d5839b16abb4e5314cc0f7a602ac8981/metta/hol/calculi-converter.metta#L408-L431

In particular, the test case of that issue comes from the reduction rule for combinator W.

[vsbogd]

@ngeiswei does the following type definition suits your needs and fixes the example?

(: λ (-> Variable Atom Atom))

[ngeiswei]

I've tried the following

1. No type definition of λ

   (= ((λ $x $f) $y) (let ($νx $νf) (sealed ($x) ($x $f)) (let $νx $y $νf)))
   !((λ $n (λ $f (λ $x ($f (($n $f) $x))))) (λ $f (λ $x $x)))

   outputs

   [(λ $f (λ $x ($f $x))), (λ $f (λ $x ($f $x))), (λ $f (λ $x ($f $x))), (λ $f (λ $x ($f $x))), (λ $f (λ $x ($f $x))), (λ $f (λ $x ($f $x))), (λ $f (λ $x ($f $x))), (λ $f (λ $x ($f $x)))]

   which is correct because ((λ $n (λ $f (λ $x ($f (($n $f) $x))))) (λ $f (λ $x $x))) represents the successor of 0, which is 1, encoded by (λ $f (λ $x ($f $x))). It's just that it is duplicated 8 times.

2. Type definition of λ with Atom

   (: λ (-> Variable Atom Atom))
   (= ((λ $x $f) $y) (let ($νx $νf) (sealed ($x) ($x $f)) (let $νx $y $νf)))
   !((λ $n (λ $f (λ $x ($f (($n $f) $x))))) (λ $f (λ $x $x)))

   outputs

   [(λ $f (λ $x ($f (((λ $f (λ $x $x)) $f) $x))))]

   which is incorrect likely because ((λ $f (λ $x $x)) $f) never gets to be reduced due to the type signature of λ.

3. Type definition of λ with type variable

   (: λ (-> Variable $a $a))
   (= ((λ $x $f) $y) (let ($νx $νf) (sealed ($x) ($x $f)) (let $νx $y $νf)))
   !((λ $n (λ $f (λ $x ($f (($n $f) $x))))) (λ $f (λ $x $x)))

   outputs

   [(λ $f (λ $x ($f (Error (((λ $f (λ $x $x)) $f) $x) "Too many arguments")))), (λ $f (λ $x ($f (Error (((λ $f (λ $x $x)) $f) $x) "Too many arguments")))), (λ $f (λ $x ($f (Error (((λ $f (λ $x $x)) $f) $x) "Too many arguments")))), (λ $f (λ $x ($f (Error (((λ $f (λ $x $x)) $f) $x) "Too many arguments"))))]

   which looks like a bug.

[vsbogd]

Type signature in this case should be different I believe. Three options below work, but they mean that second argument is evaluated before calculating lambda and this prevents constructing lambda in cl2lc function you wrote:

(: λ (-> Variable $a (-> $b $t)))
;(: λ (-> Variable $a %Undefined%))
;(: λ (-> Variable %Undefined% (-> $b $t)))

[vsbogd]

We can write a version of cl2lc which returns a correct result even when lambda type is %Undefined% using quote. But issue is that when this result is returned it is evaluated further and when it has expressions like (($f $x) ($g $x)) inside (as in ((λ $f (λ $g (λ $x (($f $x) ($g $x))))) (λ $x#1 (λ $y#1 (λ $z#1 ($x#1 ($y#1 $z#1))))))) it will be incorrectly evaluated.

Adding Atom into a lambda signature prevents sub-expressions from evaluations when it is needed. Actually I don't see why (: λ (-> Variable Atom (-> $a $t)))) doesn't work in practice. Will look at it.