Формализация регулярных выражений с операцией дополнения

Question

Я играю с формализацией сертифицированного регулярного выражения в Idris (я считаю, что та же проблема сохраняется в любом из методов теории доказательств, таких как Agda and Coq) m зациклился на том, как определить семантику операции дополнения. У меня есть следующий тип данных для представления семантики регулярных выражений:

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) 

Моя проблема заключается в представлении тип НЕВЫП конструктора, так как он имеет не строго положительное возникновение InRegExp в связи с использованием Not. Так как такие типы данных могут использоваться для определения функций без конца, они отбрасываются с помощью проверки завершения. Я хотел бы определить такую ​​семантику так, чтобы она была принята с помощью проверки окончания Idris.

Есть ли способ, которым я мог бы представить семантику операции дополнения без отрицательных вхождений InRegExp?

Answer 1

Вы можете взаимно определить 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) 

Answer 2

Вы также могли бы определить этот тип рекурсией по RegExp плюс некоторые индуктивного типа данных для семантики Star.

Я предполагаю, что он не будет взаимодействовать так же хорошо со встроенным шаблоном, но он будет иметь тот же принцип индукции.

Answer 3

Вы можете определить 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)) 

Это имеет значение, а я не вижу никаких недостатков в Это.