使用补码操作形式化正则表达式

Question

我正在使用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构造函数的类型,因为它有一个非严格正发生InRegExp因使用Not.由于这些数据类型可用于定义非终止函数,因此它们会被终止检查程序拒绝.我想以Idris终止检查器接受的方式定义这样的语义.

有没有什么方法可以代表补充操作的语义而不会出现负面影响InRegExp？

Answer 1

您可以InRegex通过递归来定义Regex.在这种情况下,严格的积极性不是问题,但我们必须在结构上进行:

import Data.List.Quantifiers

data Regex : Type where
  Chr  : Char -> Regex
  Eps  : Regex
  Cat  : Regex -> Regex -> Regex
  Alt  : Regex -> Regex -> Regex
  Star : Regex -> Regex
  Comp : Regex -> Regex

InRegex : List Char -> Regex -> Type
InRegex xs (Chr x)     = xs = x :: []
InRegex xs Eps         = xs = []
InRegex xs (Cat r1 r2) = (ys ** (zs ** (xs = ys ++ zs, InRegex ys r1, InRegex zs r2)))
InRegex xs (Alt r1 r2) = Either (InRegex xs r1) (InRegex xs r2)
InRegex xs (Star r)    = (yss ** (All (\ys => InRegex ys r) yss, xs = concat yss))
InRegex xs (Comp r)    = Not (InRegex xs r)

Star如果我们想要使用旧的定义,我们需要一个归纳类型.以下显然不起作用:

InRegex xs (Star r) = InRegex (Alt Eps (Cat r (Star r)))

但是,我们可以简单地更改定义并使有限性显式化:

InRegex xs (Star r) = (yss ** (All (\ys => InRegex ys r) yss, xs = concat yss))

这具有预期的含义,我认为没有任何缺点.

Answer 2

您可以相互定义NotInRegExp哪个可以解释regexp无法识别的含义(我还没有检查这是否是有效的语法).

data NotInRegExp : List Char -> RegExp -> Type where
 NotInEps : Not (xs = []) -> NotInRegExp xs Eps
 NotInChr : Not (xs = [ a ]) -> NotInRegExp xs (Chr a)
 NotInCat : (forall xs ys, zs = xs ++ ys ->
             NotInRegExp xs l
            + InRegExp xs l * NotInRegExp ys r) ->
            NotInRegExp zs (Cat l r)
etc...

然后,您应该能够定义一个很好的决策过程:

check : (xs : List Char) (e : RegExp) -> Either (InRegexp xs e) (NotInRegexp xs e)