Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

How to emulate lambda calculus? #39

Open
ngeiswei opened this issue Feb 27, 2024 · 17 comments
Open

How to emulate lambda calculus? #39

ngeiswei opened this issue Feb 27, 2024 · 17 comments
Labels
tutorial Tutorial question

Comments

@ngeiswei
Copy link
Collaborator

ngeiswei commented Feb 27, 2024 •
edited
Loading

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
Copy link
Collaborator

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
Copy link
Collaborator

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

@ngeiswei
Copy link
Collaborator Author

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
Copy link
Collaborator Author

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

@ngeiswei
Copy link
Collaborator Author

ngeiswei commented Feb 27, 2024 •
edited
Loading

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
Copy link
Collaborator Author

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

@Adam-Vandervorst
Copy link
Collaborator 

(= ((λ $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
Copy link

The English is the desired requirement for seal, yes!

@ngeiswei
Copy link
Collaborator Author

ngeiswei commented Feb 28, 2024 •
edited
Loading

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
Copy link
Contributor

vsbogd commented Feb 28, 2024

@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
Copy link
Contributor

vsbogd commented Feb 28, 2024 

(= ((λ $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
Copy link
Collaborator Author

ngeiswei commented Feb 28, 2024 •
edited
Loading

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 vsbogd mentioned this issue Feb 28, 2024
Merged
@vsbogd
Copy link
Contributor

vsbogd commented Feb 28, 2024

@ngeiswei it should work in a following form on the branch from trueagi-io/hyperon-experimental#609:

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

@vsbogd
Copy link
Contributor

vsbogd commented Feb 28, 2024

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
Copy link
Collaborator Author

ngeiswei commented Feb 28, 2024 •
edited
Loading

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
Copy link
Collaborator Author

@ngeiswei it should work in a following form on the branch from trueagi-io/hyperon-experimental#609

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

vsbogd added a commit to vsbogd/metta-examples that referenced this issue Mar 1, 2024
@vsbogd
Use seal to patch SICP and combinators examples for minimal MeTTa
0c7e768 
Implementing lambda requires variables with restricted scope, see
trueagi-io#39
@vsbogd
Copy link
Contributor

vsbogd commented Mar 1, 2024

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

@Necr0x0Der Necr0x0Der added the tutorial Tutorial question label Mar 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
tutorial Tutorial question
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
5 participants
@leithaus @ngeiswei @vsbogd @Adam-Vandervorst @Necr0x0Der