首页 文章

这个递归函数不是完全的，还是编译器无法证明它？如何将其重写为总计？

提问于
浏览 次
0

出现以下代码时：

module TotalityOrWhat

%default total

data Instruction = Jump Nat | Return Char | Error

parse : List Char -> Instruction
parse ('j' :: '1' :: _) = Jump 1
parse ('j' :: '2' :: _) = Jump 2
parse ('j' :: '3' :: _) = Jump 3
parse ('r' :: x :: _) = Return x
parse _ = Error

parseDriver : String -> Maybe Char
parseDriver = parseDriver' . unpack where
  parseDriver' : List Char -> Maybe Char
  parseDriver' xs =
    case parse xs of
      (Jump j) => parseDriver' $ drop j xs
      (Return x) => Just x
      Error => Nothing

伊德里斯给出了一个错误：

TotalityOrWhat.idr：17：3：
由于递归路径，TotalityOrWhat.parseDriver，parseDriver'可能不完全
TotalityOrWhat.parseDriver，parseDriver' - > TotalityOrWhat.parseDriver，parseDriver'

TotalityOrWhat.idr：15：1：
TotalityOrWhat.parseDriver可能不是全部由于：
TotalityOrWhat.parseDriver，parseDriver'

我已经用其他几种方式重写了这段代码，但是无法让Idris将其识别为总数 . 我错了它是完全的，还是伊德里斯不能确定它是什么？如果它本质上是完全的，我怎么能重写它以便伊德里斯将它识别为总数？

recursion pattern-matching idris totality

2 回答

  • 3

    这不是“为什么它不被认为是完全”的答案，甚至不是“如何将其改为被认可为总数”的答案，但是因为你提到了

    我已经用其他几种方式重写了这段代码，但是无法让Idris将其识别为总数，

    我以为你可能对解决方法感兴趣 . 如果您手动将 parse 内联到 parseDriver' ，您可以通过整体检查器获取它：

    total parseDriver : String -> Maybe Char
parseDriver = parseDriver' . unpack where
  parseDriver' : List Char -> Maybe Char
  parseDriver' ('j' :: '1' :: xs) = parseDriver' ('1' :: xs)
  parseDriver' ('j' :: '2' :: xs) = parseDriver' xs
  parseDriver' ('j' :: '3' :: _ :: xs) = parseDriver' xs
  parseDriver' ('r' :: x :: _) = Just x
  parseDriver' _ = Nothing

    这是有效的，因为我们总是在 xs 的某些后缀上进行结构上的递归 .

    回复于
  • 3

    这里的问题是Idris无法知道 drop j xs 从输入中产生了一个严格较小的列表，因为 drop 's type isn' t足够表达 .

    因此，另一种特殊方法是使用伪参数，通过在递归调用 parseDriver' 时使用结构上较小的列表 xs' ，使得整体检查器接受该函数 .

    parseDriver : String -> Maybe Char
parseDriver s = parseDriver' chars chars where
  chars : List Char
  chars = unpack s

  -- 2nd parameter is a dummy one (to make totality checker happy)
  parseDriver' : List Char -> List Char -> Maybe Char
  parseDriver' _  [] = Nothing
  parseDriver' xs (_::xs') =
    case parse xs of
      Jump j => parseDriver' (drop j xs) xs'
      Return x => Just x
      Error => Nothing

    我们也可以使用一些自然参数 n ，我们可以在每一步减少，确保我们停在 0 . n 的初始值自然可以是输入列表的长度 .

    回复于

相关问题