@authors: Many thanks for preparing the online presentation. (Could you, please, indicate if/when you are online and see this by posting a ping message here?)
@audience: Please post your questions and comments here.
I am an outsider of this topic. Is there any general criterion on which equational theorem should be turned into code? For example, an equation like f(x)=f(x) is obviously useless as code. Is it totally up to the user?
It is totally up to the user. The Isabelle only objects if the equations do not have the right format for a functional language (eg non-constructors in patterns) This is the beauty of it (we can generate non-terminating code, eg an interpreter) but it also means that we can only guarantee partial correctness.
@authors: Many thanks for preparing the online presentation. (Could you, please, indicate if/when you are online and see this by posting a ping message here?)
ReplyDelete@audience: Please post your questions and comments here.
I am online.
ReplyDeleteThe flash video works with Firefox under Linux.
Tobias
Hi,
ReplyDeleteI am an outsider of this topic.
Is there any general criterion on which equational theorem should be turned into code?
For example, an equation like f(x)=f(x) is obviously useless as code.
Is it totally up to the user?
It is totally up to the user. The Isabelle only objects if the equations do not have the right format for a functional language (eg non-constructors in patterns) This is the beauty of it (we can generate non-terminating code, eg an interpreter) but it also means that we can only guarantee partial correctness.
ReplyDeleteThanks for the question.