How to emulate lambda calculus?

ngeiswei commented 4 months ago

What is your problem?

I cannot emulate lambda calculus, I would say due to a lack of support for scopes in MeTTa.

How to reproduce your problem?

Run the following code

(= ((λ $x $f) $y) (let $x $y $f))
!((λ $x ($x $x)) (λ $y ($y $y)))

What do you get?

It outputs [].

What would you want to get instead?

It should never halt, as per the mockingbird infinite loop (M M).

Why do you think that is?

The problem comes the fact that

((λ $x ($x $x)) (λ $y ($y $y)))

reduces to

(let $x (λ $y ($y $y)) ($x $x))

which reduces to

((λ $y ($y $y)) (λ $y ($y $y)))

which finally reduces to

(let $y (λ $y ($y $y)) ($y $y))

which fails because $y does not unify with (λ $y ($y $y)).

You can see that this is caused by the absence of alpha-conversion, because λ is not treated as a scope.

What other questions do you have?

Do we need scopes in MeTTa?

If the answer is no, then how to emulate lambda calculus in MeTTa?

Adam-Vandervorst commented 4 months ago

This is solved by sealing the arguments in respective scopes, which would split $y in the final reduction step (disallowing non-local unification, but also enabling the individual reductions).

Adam-Vandervorst commented 4 months ago

There may be a workaround with a drawname grounded function that gives you a fresh variable to use in the beta reduction.

ngeiswei commented 4 months ago

There may be a workaround with a drawname grounded function that gives you a fresh variable to use in the beta reduction.

Right! So I suppose you mean something like

(= ((λ $x $f) $y) (let ($νx $νy $νf) (alpha-convert ($x $y $f)) (let $νx $νy $νf)))

That's a great suggestion, although I feel we may still want to consider adding a built-in scope or sealing (if there's a difference).

ngeiswei commented 4 months ago

Oh, actually that doesn't work either in my test case :-(, maybe you meant something else...

ngeiswei commented 4 months ago

Actually I think it does work! But the code should be

(= ((λ $x $f) $y) (let ($νx $νf) (alpha-convert ($x $f)) (let $νx $y $νf)))

i.e. no need to alpha-convert $y.

ngeiswei commented 4 months ago

@Adam-Vandervorst, would you mind showing how the solution using seal would look like?

Adam-Vandervorst commented 4 months ago

(= ((λ $x $f) $y) (let $x $y $f)))

!((seal (, $x) (λ $x ($x $x))) ((seal (, $y) (λ $y ($y $y))))

(let $x (λ $y1 ($y1 $y1)) ($x $x))

((λ $y ($y $y)) (λ $y1 ($y1 $y1)))

(let $y (λ $y1 ($y1 $y1)) ($y $y))

...

Basically (seal (, v1 v2 ... vn) <body>) says "when you're evaluating body, vk will not be accessible outside of " i.e. it makes the variables anonymous.

leithaus commented 4 months ago

The English is the desired requirement for seal, yes!

ngeiswei commented 4 months ago

I see... You've automatically alpha-converted $y to $y1 to avoid name collision but it's not super clear how. I suppose what you meant was more something like

((seal (, $x) (λ $x ($x $x))) ((seal (, $y) (λ $y ($y $y))))

rewrites into

(seal (, $x) (let $x (seal (, $y) (λ $y ($y $y))) ($x $x)))

which rewrites into (note how the outer (seal (, $x) ...) will disappear since $x no longer appears in the body),

((seal (, $y) (λ $y ($y $y))) (seal (, $y) (λ $y ($y $y))))

which is OK because $y of the first mockingbird operator is sealed from the $y of the second one. If we keep going we get

(seal (, $y) (let $y (seal (, $y) (λ $y ($y $y))) ($y $y)))

Then MeTTa needs to unify $y with (seal (, $y) (λ $y ($y $y))) which it can because $y in the right term is sealed.

But I wonder how is seal different than a regular scope?

vsbogd commented 4 months ago

@ngeiswei , thanks for raising it again. We already had a workaround for this in old Rust interpreter thus your code will work correctly with minimal MeTTa disabled. In minimal MeTTa let is implemented using unify thus this issue raises again. But I think we need to implement a long term solution this time.

I like your suggestion:

Actually I think it does work! But the code should be
(= ((λ $x $f) $y) (let ($νx $νf) (alpha-convert ($x $f)) (let $νx $y $νf)))
i.e. no need to alpha-convert $y.

It should work exactly as previous let workaround, but adding alpha-convert allows us introducing scoping in any context we need it. I will try adding quick implementation to check whether it works as expected.

vsbogd commented 4 months ago

(= ((λ $x $f) $y) (let $x $y $f)))

!((seal (, $x) (λ $x ($x $x))) ((seal (, $y) (λ $y ($y $y))))

(let $x (λ $y1 ($y1 $y1)) ($x $x))

((λ $y ($y $y)) (λ $y1 ($y1 $y1)))

(let $y (λ $y1 ($y1 $y1)) ($y $y))

...
Basically (seal (, v1 v2 ... vn) <body>) says "when you're evaluating body, vk will not be accessible outside of " i.e. it makes the variables anonymous.

In hyperon-experimental all variables inside λ are anonymous already. One can say each call has body variables sealed. Thus in fact ((λ $y ($y $y)) (λ $y ($y $y))) is unified with (= ((λ $x#1 $f#1) $y#1) (let $x#1 $y#1 $f#1)). But after unification we have { $y == $x#1 } and finally we have (let $y (λ $y ($y $y)) ($y $y)).

But we could use sealing inside let I believe in a way which is suggested by @ngeiswei:

(= ((λ $x $f) $y) (let ($νx $νf) (seal (, $x) ($x $f)) (let $νx $y $νf)))

ngeiswei commented 4 months ago

It indeed works with the old MeTTa. ~@vsbogd, could briefly explain why? What is the workaround in question?~

Ah, you've already answered that above.

vsbogd commented 4 months ago

@ngeiswei it should work in a following form on the branch from https://github.com/trueagi-io/hyperon-experimental/pull/609:

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

vsbogd commented 4 months ago

We can implement it as sealed which generates random variable names and replaces variables or as alpha-conversion + new-var which decouples generating var and variable renaming. I am not sure what is the best option.

ngeiswei commented 4 months ago

I don't know either. Somewhat perhaps related, after reading @leithaus Transparent MeTTa proposals, I wonder if we wouldn't want to replace variables by a quotation construct @ which would allow to give variables structure. That way alpha-conversion could be implemented in pure MeTTa. There are other use cases, for instance I wanted to have two types of variables in the backward chainer, one for program holes, one for program variables (like in Idris, ?x is a hole while x is a variable).

If we don't want to depart from $ as variable indicator, then $ could simply be used on expressions such as $(x y), etc.

ngeiswei commented 4 months ago

@ngeiswei it should work in a following form on the branch from https://github.com/trueagi-io/hyperon-experimental/pull/609

Wow, I confirm that it solves the problem on my end.

vsbogd commented 4 months ago

SICP and combinator logic examples also suffer from this. Possible fix which uses non-merged seal is in my private branch https://github.com/vsbogd/metta-examples/tree/minimal-seal-patch

trueagi-io / metta-examples