[isabelle] A problem on termination of a higher-order fun... · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A problem on termination of a higher-order fun...

Email Gateway (Aug 22 2022 at 08:58):

From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear experts:

I meet a problem on the termination of a function, which is due to higher-order function:( map) and
(may be) uniterpretated functions. I really appreciate if you can do me a favour.

theory test imports Main Finite_Set
begin
datatype varType=Global string | Para string nat

consts oracleFunInterPretation::"string \<Rightarrow> nat list \<Rightarrow>nat"
oraclePredInterPretation::"string \<Rightarrow> nat list\<Rightarrow>bool"

function expEval :: " state\<Rightarrow> expType \<Rightarrow> nat" and
formEval :: " state\<Rightarrow>formula \<Rightarrow>bool" where

evalIVar:"expEval s (IVar ie) = ( s ie)" |
evalConst:"expEval s (Const i) = i" |
evalIndex:"expEval s (Index i) = i" |
evalIteForm:"expEval s (iteForm f e1 e2)=
( if (formEval s f ) then (expEval s e1)
else (expEval s e2 ))" |
evalFunExp:"expEval s (funExp opStr exps)=
(if (opStr=''+'') then (expEval s (exps!0) ) + (expEval s (exps!1) )
else (expEval s (exps!0) ) - (expEval s (exps!1) ))" |
evalOracleFunExp:"expEval s (oracleFun opStr exps) = oracleFunInterPretation opStr (map (expEval s) exps)"|

evalOraclePred:"formEval s (oraclePred opStr exps)= oraclePredInterPretation opStr (map (expEval s) exps)"|
"formEval s (pred opStr exps)=
(if (opStr=''<'') then (expEval s (exps!0) ) < (expEval s (exps!1) )
else if (opStr=''>'') then (expEval s (exps!0) ) > (expEval s (exps!1) )
else True)" |
evalExp: "formEval s (eqn e1 e2)= ((expEval s e1 ) = (expEval s e2 ))" |
evalAnd: "formEval s ( andForm f1 f2) =( (formEval s f1 ) \<and> (formEval s f2 ))"|
evalNeg: "formEval s (neg f1 ) = ( \<not>(formEval s f1 ))"|
evalOr: "formEval s (orForm f1 f2) =( (formEval s f1 ) \<or> (formEval s f2 ))"|
evalImp:"formEval s (implyForm f1 f2) = ( (formEval s f1 ) \<longrightarrow> (formEval s f2 ))" |
"formEval s chaos =True"

by pat_completeness auto
termination by lexicographic_order

For your convenience, I also attaches the file.

regards!

lyj238@ios.ac.cn
test.thy

Email Gateway (Aug 22 2022 at 08:58):

From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear experts:

I meet a problem on the termination of a function, which is due to higher-order function:( map) and
(may be) uniterpretated functions. I really appreciate if you can do me a favour.

theory test imports Main Finite_Set
begin
datatype varType=Global string | Para string nat

consts oracleFunInterPretation::"string \<Rightarrow> nat list \<Rightarrow>nat"
oraclePredInterPretation::"string \<Rightarrow> nat list\<Rightarrow>bool"

function expEval :: " state\<Rightarrow> expType \<Rightarrow> nat" and
formEval :: " state\<Rightarrow>formula \<Rightarrow>bool" where

by pat_completeness auto
termination by lexicographic_order

For your convenience, I also attaches the file.

regards!

lyj238@ios.ac.cn
test.thy

Email Gateway (Aug 22 2022 at 08:59):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
The problem is that your function might indeed not terminate. The problem is that your
case for funExp takes a list of subexpressions, but there are no checks that there are
indeed sufficiently many operands in the list (which you access with ! 0 and ! 1). If,
say, the list of subexpressions is empty, then ! 0 is not specified and could in theory
return the same expression again. Either you change your datatype to make sure that there
are always sufficiently many operands or include checks in the function definition.

Hope this helps,
Andreas

Email Gateway (Aug 22 2022 at 08:59):

Hope this helps,
Andreas

Email Gateway (Aug 22 2022 at 08:59):

From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Thanks，

I modify the thy file as you pointed out

it does work now.

lyj238@ios.ac.cn
test.thy

Last updated: Apr 20 2024 at 08:16 UTC