Add sealed operation

[vsbogd]

Replaces #512. Add (sealed (<vars>) <atom>) grounded operation which replaces all occurences of any var from <vars> inside <atom> by unique variable.

sealed can be used to create a locally scoped variables, see https://github.com/trueagi-io/metta-examples/issues/39#issuecomment-1968809328 as an example.

[vsbogd]

@cowboyphilosopher FYI

[luketpeterson]

I don't understand the use case as well as @cowboyphilosopher so I don't want to comment on whether this addresses the need or fits within the design of MeTTa.

Regarding the code it looks fine. @vsbogd I am however wondering why you changed the ReplacingMapper to the CachingMapper; whether the desire to have an input type that was different from the output type was fundamental / philosophical, or whether it was just made the code more manageable inside the implementation of SealedOp

[vsbogd]

whether the desire to have an input type that was different from the output type was fundamental / philosophical, or whether it was just made the code more manageable inside the implementation of SealedOp

Thanks for asking Luke. It is the change I doubt about. Main reason is to have universal "mapper" implementation which suits both cases:

• collecting atoms without replacing (which are most of the cases in code)
• collecting atoms with replacing (the case of the SealedOp)

When I tried to change ReplacingMapper to cover both cases I have found that first case is not implementable in Rust without additional cloning. After that I thought that maybe compiler will optimize out this cloning after applying the function type parameter. Now I think I could implement second just by getting mapping_mut() and adding vars manually.

I think I will check whether compiler optimizes this and if not then re-implement SealedOp using mapping_mut.

[vsbogd]

Also discussed with @Necr0x0Der that alpha-conversion is more universal operation, so may be it is worth to reimplement sealed using alpha-conversion.

[vsbogd]

I don't understand the use case

It is used to implement beta reduction. For example one need to replace variable $x in expression $f by some value. In MeTTa it is written using let (let $x <value> $f). But when value contains $x this does not work. In (let $x (p $x) $f) variable $x cannot be unified with (p $x). On the other hand it is a legal case to replace $x by (p $x) inside $f.

To resolve this we can use alpha conversion. Replace variable $x inside $f by an anonymous variable $x#1 and then do (let $x#1 (p $x) $f). Now $x#1 can be unified with (p $x) and beta reduction is successful.

sealed is a combination of alpha conversion and introducing of the a anonymous variable.

(= (sealed $var $atom)
  (alpha-convert $var (new-var) $atom))

in case of a single variable.

[vsbogd]

One more lambda example is https://github.com/trueagi-io/metta-examples/pull/33 which cannot be run using minimal MeTTa, because minimal interpreter implemented in MeTTa accurately keeps track of variable values. As result map and lambda... functions doesn't work without being sealed.

[ngeiswei]

Could someone resolve the conficts with the main branch? Or even better, merge it (if we agree that it is correct)?

[luketpeterson]

Feel free to merge, @vsbogd if you think it's ready.