Re: [isabelle] computation_check with "let ... in ..."



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


Am 21.02.2018 um 15:19 schrieb Wenda Li:
> 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
> 
>> On 21 Feb 2018, at 08:33, Thiemann, Rene <Rene.Thiemann at uibk.ac.at> wrote:
>>
>> 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é
>>
>>
>>
>>> Am 20.02.2018 um 22:00 schrieb Wenda Li <wl302 at 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
>>>
>>
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.