Email Gateway (Aug 22 2022 at 12:20): Email Gateway (Aug 22 2022 at 12:20):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hello,
I have a certain structure F(p,f) from F_Type where p is a predicate on
tuples
and f is a function on tuples with tuples as values.
I have a set of operations on F_Type that reduces to operations of
predicates and functions. For example I have a composition on
F_Type that, when applied to F(p,f) and F(p',f') reduces to:
F(p,f) comp F(p',f') = F(inf p (p' o f), f o f')
I have also more complicated operations, and they all are
reduced to a composition of functions. The sizes of the tuples
are not fixed, and some of the operations change the
size of the tuples.
I have an expression of Fs and composition operators, and my
goal is to simplify it to F(p,f), and have p and f as simple as possible.
The main problem is that the tuples could be quite large (160 components
for some example), and simplifying functions over these tuples
seems very slow.
So far I came up with the following simplification pattern:
I use the format "\lambda (x,y,z) . (x+y, x*x, z - 1)" as the canonical
format for functions (and predicates), and whenever I compose
F(p,f) comp F(p',f')
I compute p'', and f'' in canonical form such that
F(p'', f'') = F(p,f) comp F(p',f'),
and I prove this as a theorem.
In order to compute f'', I take f o f' and I apply it to the tuple
(x,y,z,...), I simplify it and I get the theorem
(A) "/\ x y x ... . (f o f') (x,y,z,...) = some expression on x, y, z"
and from this I abstract to
(B) "f o f' = (\lambda (x,y,z, ...) . some expression on x, y, z)"
To get from (A) to (B), I construct dynamically a specific theorem for
the tuple (x,y,z,...)
The questions are:
Is there a more efficient representation of functions on tuples
that I can use?
Is it possible to get from (A) to (B) using a generic theorem?
Best regards,
Viorel Preoteasa
Last updated: Apr 27 2024 at 01:05 UTC