some combinator logic experiments added

[CICS-Oleg]

There are some questions in y_comb_examples.metta.

[vsbogd]

To define Y combinator one can redefine BCKW combinators properly:

(= (((B $x) $y) $z) ($x ($y $z)))
(= (((C $x) $y) $z) (($x $z) $y))
(= ((K $x) $y) $x)
(= ((W $x) $y) (($x $y) $y))

After this all tests will pass in their original form:

!(assertEqual
  (((((S (K S)) K) x) y) z)
  (((B x) y) z))

!(assertEqual
    (((((S ((S (K ((S (K S)) K))) S)) (K K)) x) y) z)
    (((C x) y) z))

!(assertEqual
    ((((S S) (S K)) x) y)
    ((W x) y))

!(assertEqual
    (((S I) I) a)
    (a a))

and one can define U and Y:

(= (U $x) (((S I) I) $x))
(= (Y $x) (((B U) ((C B) U)) $x))

It is possible to implement recursive functions using Y like this:

(: id' (-> Atom (-> $t $t)))
(= ((id' $f) $x) $x)
(= (id $x) ((Y id') $x))
!(assertEqual (id A) A)

(: fac (-> Atom (-> Int Int)))
(= ((fac $f) $x) (if (> $x 0) (* $x ($f (- $x 1))) 1))
(= (fact $x) ((Y fac) $x))
!(assertEqual (fact 0) 1)
!(assertEqual (fact 5) 120)

It is important to have first argument of type Atom otherwise the example will fall into infinite recursion.

I also have no success with lambdas:

(: lambda (-> Variable Atom (-> Atom Atom)))
(= ((lambda $var $body) $val)
    (let $var $val $body))

(= (id' $x) ((Y (lambda $f (lambda $x $x))) $x))
!(assertEqual ((lambda $x $x) A) A)
;!(assertEqual (id' A) A)

(= (fact' $y)
  (let $fac (lambda $f
    (let $fac' (lambda $x (if (> $x 0) (* $x ($f (- $x 1))) 1)) $fac') )
      ((Y $fac) $y) ))
;!(assertEqual (fact' 0) 1)
;!(assertEqual (fact 5) 120)

Looks like somehow these implementations fall into infinite recursion anyway.

[vsbogd]

Ok finally it is clear the reason is that lambda has many places to fall into infinite recursion and we need to close them all. @CICS-Oleg I have raised PR with changes which I commented above so you can just merge it if you will to apply these changes https://github.com/CICS-Oleg/metta-examples/pull/1. I dropped parax example because I am not sure if it is needed. If you think so please shout - I will return it again.

[vsbogd]

Finally found one more issue. Values from application of the lambda sneaks into definition of the lambda. It sounds like a bug in the code of the interpreter.

[CICS-Oleg]

@vsbogd Thank you so much for that clear explanation.

[vsbogd]

Merged it, thank you for the examples!