Email Gateway (Aug 22 2022 at 16:50): Email Gateway (Aug 22 2022 at 16:50):From: Wenda Li <wl302@cam.ac.uk>
Dear code generation experts,
I was wondering how can we computation_check a term with the form “let … in …”. Here is a small example: given a proposition that can be proved by evalutaion (i.e., by eval or by by code_simp),
lemma "let x ::int poly= [:2,3:] in [:1,2:] * x = [:2, 7, 6:]”
I want to solve it using the computation_check mechanic. If I unfold the “let” constant first, the proposition can be proved like the following:
ML ‹
val holds = @{computation_check terms:
Trueprop
"times::int poly ⇒ _"
"HOL.equal ::int poly ⇒ _"
"0 :: int poly"
"pCons :: int ⇒ _"
"0 :: int" "1 :: int"
Code_Target_Int.positive datatypes:num
};
›
lemma "let x::int poly= [:2,3:] in [:1,2:] * x = [:2, 7, 6:]"
unfolding Let_def
apply (tactic ‹
CONVERSION (holds @{context}) 1
›)
by (rule TrueI)
However, without the unfolding (i.e., remove “unfolding Let_def”), "apply (tactic ‹CONVERSION (holds@{context}) 1›)” will get stuck. I am not sure if there is any other constant I should add to “@{computation_check terms:
...
};"
to make the CONVERSION work.
Thanks in advance,
Wenda
signature.asc
Email Gateway (Aug 22 2022 at 16:50):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Wenda,
one might be tempted to just add “Let" to the list of constants. However,
this still won’t work since your input term contains an abstraction:
Let [:2,3:] (% x. [:1,2:] * x = [:2, 7, 6:])
And according to the code-generator manual (codegen.pdf), abstractions are not supported:
From the documentation:
6.5 Pitfalls concerning input terms
No abstractions. Only constants and applications are admissible as input; abstractions are not possible. In theory, the compilation schema could be extended to cover abstractions also, but this would increase the trusted code base. If abstractions are required, they can always be eliminated by a dedicated preprocessing step, e.g. using combinatorial logic.
So your unfolding of the “Let” constant is precisely such a required preprocessing step to get rid of the abstraction in this example.
With best regards,
René
Email Gateway (Aug 22 2022 at 16:51):From: Wenda Li <wl302@cam.ac.uk>
Dear René,
Thanks for your prompt reply and detailed explanation, which did clarify some of my confusions.
Eliminating occurrences of “let … in …” when pre-prossessing is of course a viable way, but my main motivation for this “let … in …” expression is possible gain in performance: suppose we want to prove the following proposition
lemma "let x::int poly= smult 2 [:1,2:] in [:2,3:] * x * x = [:8, 44, 80, 48:]”
through evaluation. If we can directly evaluate "let x::int poly= smult 2 [:1,2:] in [:2,3:] * x * x = [:8, 44, 80, 48:]” in SML, we probably need to do the “smult” operation only once. However, with the “let” expression unfolded, what we need to evaluate is instead
[:2, 3:] * smult 2 [:1, 2:] * smult 2 [:1, 2:] = [:8, 44, 80, 48:]
, with which I guess the “smult” operation will be carried out twice.
To sum up, my main purpose of “let … in …” is to eliminate repeated computations, and I hope to achieve this in the computation_check setups.
Many thanks,
Wenda
signature.asc
Email Gateway (Aug 22 2022 at 16:51):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Wenda,
a generic solution to the abstraction issue would be a preprocessor
transforming abstractions into expressions in combinatorial logic.
There is an implementation of this in meson:
ML ‹
Meson_Clausify.introduce_combinators_in_cterm @{context}
@{cterm "let (k::int) = 42 * 7 in k + k * 1705 - k ^ 2"}
›
Unfortunately, following the comments in the code, the implementation
seems suboptimal.
I would appreciate if someone would use this as a base to provide a
generic preprocessor in Pure; this could then be an official part of
computations.
Cheers,
Florian
signature.asc
Last updated: Apr 25 2024 at 01:08 UTC