用补集操作规范正则表达式

Question

用补集操作规范正则表达式

4

我正在使用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的负面影响？

- Rodrigo Ribeiro

3个回答

5

您可以相互定义NotInRegExp，这将解释什么是不被正则表达式识别（我还没有检查过这是否是有效的语法）。

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)

- gallais

谢谢。你说得完全正确！这个解决方案简单而优雅。 - Rodrigo Ribeiro

@RodrigoRibeiro FYI，我已经修复了我定义的NotInCat构造函数中的一个错误。 - gallais

3

你可以通过对正则表达式进行递归定义，再加上一些关于Star语义的归纳数据类型来定义这种类型。

我猜它不能与内置的模式匹配很好地交互，但它具有相同的归纳原理。

- Saizan

抱歉，我不明白您的意思。您是在说我应该将InRegExp定义为类型为RegEx -> Type的函数，并为Kleene星定义归纳类型吗？ - Rodrigo Ribeiro

一个类型为 "List Char -> RegExp -> Type" 的函数，但是是的。 - Saizan

糟糕...我的意思是List Char -> RegExp -> Type... :) 感谢您的建议。 - Rodrigo Ribeiro

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- András Kovács · Accepted Answer

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

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))

这个表达意思恰当，我没有看到任何缺点。