What is your problem? I cannot emulate lambda calculus, I would sa

Actually I think it does work! But the code should be <div class="snippet-clipboa

<a class="user-mention notranslate" data-hovercard-type="user" data-hovercard-url="/us

<div class="snippet-clipboard-content notranslate position-relative overflow-auto" data

<a class="user-mention notranslate" data-hovercard-type="user" data-hover

<a class="user-mention notranslate" data-hovercard-type="user" data-hovercard-url="/us

<div class="snippet-clipboard-content notranslate position-relative overflow-auto" data-snippet-clip

How to emulate lambda calculus? about metta-examples HOT 17 OPEN

trueagi-io commented on August 14, 2024

How to emulate lambda calculus?

from metta-examples.

Comments (17)

Adam-Vandervorst commented on August 14, 2024 2

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).

from metta-examples.

ngeiswei commented on August 14, 2024 2

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.

from metta-examples.

Adam-Vandervorst commented on August 14, 2024 1

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

from metta-examples.

vsbogd commented on August 14, 2024 1

@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.

from metta-examples.

vsbogd commented on August 14, 2024 1

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

from metta-examples.

ngeiswei commented on August 14, 2024 1

@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.

from metta-examples.

ngeiswei commented on August 14, 2024

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).

from metta-examples.

ngeiswei commented on August 14, 2024

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

from metta-examples.

ngeiswei commented on August 14, 2024

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

from metta-examples.

Adam-Vandervorst commented on August 14, 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.

from metta-examples.

leithaus commented on August 14, 2024

The English is the desired requirement for seal, yes!

from metta-examples.

ngeiswei commented on August 14, 2024

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?

from metta-examples.

ngeiswei commented on August 14, 2024

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.

from metta-examples.

vsbogd commented on August 14, 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)))

from metta-examples.

vsbogd commented on August 14, 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.

from metta-examples.

ngeiswei commented on August 14, 2024

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.

from metta-examples.

vsbogd commented on August 14, 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

from metta-examples.

How to emulate lambda calculus? about metta-examples HOT 17 OPEN

Comments (17)

Related Issues (11)

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent