Enzo Crance (Feb 27 2023 at 10:09): Enzo Crance (Feb 27 2023 at 10:09):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?
Enrico Tassi (Feb 27 2023 at 10:29):(pi x y\ copy x y :- sigma Tmp1 Tmp2\ p1 x Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 y) => copy T T'
or
(pi x y Tmp1 Tmp2\ copy x y :- p1 x Tmp1, p2 Tmp1 Tmp2, p3 Tmp2 y) => copy T T'
(the latter is faster)
Enrico Tassi (Feb 27 2023 at 10:30):The order of abstractions does not matter
Enzo Crance (Feb 27 2023 at 11:10):Thanks a lot! :smile:
Last updated: Apr 20 2024 at 12:02 UTC