我正在使用Idris进行正则表达式匹配器的认证形式化(我相信在任何基于类型论的证明助手中都存在同样的问题,例如Agda和Coq),但我卡在如何定义补集操作的语义上。我有以下数据类型来表示正则表达式的语义:
data InRegExp : List Char -> RegExp -> Type where
InEps : InRegExp [] Eps
InChr : InRegExp [ a ] (Chr a)
InCat : InRegExp xs l ->
InRegExp ys r ->
zs = xs ++ ys ->
InRegExp zs (Cat l r)
InAltL : InRegExp xs l ->
InRegExp xs (Alt l r)
InAltR : InRegExp xs r ->
InRegExp xs (Alt l r)
InStar : InRegExp xs (Alt Eps (Cat e (Star e))) ->
InRegExp xs (Star e)
InComp : Not (InRegExp xs e) -> InRegExp xs (Comp e)
我的问题是如何表示InComp构造函数的类型,因为它使用了Not,导致InRegExp出现了非严格正数。由于此类数据类型可以用来定义非终止函数,因此它们被终止检查器拒绝。我希望以一种被Idris终止检查器接受的方式定义这样的语义。
有没有一种方法可以表示补集操作的语义而不具有InRegExp的负面影响?
(a|b)*
被解释为(a*)|(b*)
(这是因为xs = concat(replicate n ys)
要求所有子匹配都相同)。 - gallaisAll (flip InRegex r) yss
。是否有一种类似的解决方案可以绕过这个问题? - Rodrigo Ribeiroflip
。已編輯。 - András Kovács