Email Gateway (Aug 19 2022 at 10:58): Email Gateway (Aug 19 2022 at 10:58):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
when I export list-based code to Scala and run it on huge inputs, it
always gives me a StackOverflowException. Looking at the stack trace
and providing the following tail-recursive version of map, everything
works fine.
fun map_tailrec :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list ⇒ 'b list" where
"map_tailrec f [] accs = accs" |
"map_tailrec f (a#as) accs = (map_tailrec f as ((f a)#accs))"
lemma map_tailrec_is_listmap:
"rev (map_tailrec f l accs) = (rev accs)@(List.map f l)"
apply(induction l accs rule: map_tailrec.induct)
apply(simp_all)
done
definition efficient_map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"efficient_map f l ≡ rev (map_tailrec f l [])"
lemma[code]: "List.map f l = efficient_map f l"
by(simp add: efficient_map_def map_tailrec_is_listmap)
Why is there no tail-recursive code equation of List.map in the default library?
Regards
Cornelius
Last updated: Apr 25 2024 at 20:15 UTC