Hello. I want to perform a substitution with
copy, where the clause added to the context has a body to compute stuff. Up to management of the scope of variables, it would look like this:
(copy X Y :- p1 X Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 Y) => copy T T'
What do I need to add? (quantifiers / which variables / what order)
Until now I have only used single line
copy instances added to the context, where the output is directly linked to the input, without further computations.
Intuitively, for the more complex case, I did the following but it doesn't seem to work:
(pi x y\ sigma Tmp1 Tmp2\ copy x y :- p1 x Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 y) => copy T T'
sigma for all variables local to the body,
pi so that the clause behaves like a top-level clause)
Did I make a mistake somewhere else, or is this code incorrect?
(pi x y\ copy x y :- sigma Tmp1 Tmp2\ p1 x Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 y) => copy T T'
(pi x y Tmp1 Tmp2\ copy x y :- p1 x Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 y) => copy T T'
(the latter is faster)
The order of abstractions does not matter
Thanks a lot! :smile:
Last updated: Jun 06 2023 at 23:01 UTC