Email Gateway (Aug 23 2022 at 08:14): Email Gateway (Aug 23 2022 at 08:14):From: hai.yang@tuta.io
Hello,
I have an Isabelle/HOL definition looks like
definition "f1 args = filter g (f0 args)",
where f0 returns a list.
Now, if I try to compute
value "f1 args0",
for a specific value of args0, this is slower than
value "f0 args0"
definition "f0args0 = <content pasted from the results obtained above>"
value "filter g f0args0"
When I have a big number of nested definitions (say f(n+1) whose definitions depend on f(n), f(n-1), ..., f0),
this problem becomes unbearable: if I try a computation involving f(n+1), it will never terminate,
while if I manually split computations as above, feeding the output of f(j) to f(j+1) by copy and paste, it will.
However, this is unbearable work for even moderately large n.
Is there something I can do about that? Or is that a fundamental limitation of functional programming?
(I'm saying that because by the copy/paste above I am formally introducing side effects, I think)
Thanks!
Hai Yang
Email Gateway (Aug 23 2022 at 08:14):From: Peter Lammich <lammich@in.tum.de>
(Sorry, I replied only privately by mistake)
Last updated: Nov 21 2024 at 12:39 UTC