Valentin Springsklee (Nov 11 2022 at 17:09): Valentin Springsklee (Nov 11 2022 at 17:09):Hello, I have a question regarding the Imperative Refinement Framework. I want to generate Code from monadic functions. I use export_code from Imperative/HOL functions as well as Sepref to automatically synthesize code from monadic functions of type nres. I want to specify functions, that are implemented as loops and I use the WHILE combinator for that.
Is it possible to generate code that uses the target language's native while keyword rather than a recursive definition of the while combinator?
Mathias Fleury (Nov 11 2022 at 17:24):while from the target language doesn't really map back to WHILET because of the types...
Valentin Springsklee (Nov 14 2022 at 11:20):Do you mean the recursive nature of the WHILE(T)-combinator's type? WHILET is a monadic function. I refined my function to the Imperative HOL combinator while :: "('a ⇒ bool) ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'a". By showing total correctes of the function that uses WHILET, monads can be eliminated. Are saying that this type cannot be mapped to an imperative while loop?
Mathias Fleury (Nov 14 2022 at 11:30):the while I know from programming languages does not take a function has second argument…
Valentin Springsklee (Nov 15 2022 at 12:19):Thanks for the answer! That was my intuition. And, it i clear, that the mapping is not direct. The Isabelle While is a function with a return value. One could informally describe the while combinator as a function that receives the termination condition and the loop body as parameters, receives an initial value and returns the result of the computation in the body. I understand, that the mapping is not trivial, especially when it must be verified. Anyway, I thought I'd ask to see if anybody had already done it.
Last updated: Apr 19 2024 at 12:27 UTC