伊莎贝尔：归纳谓词的使用

Question

我需要定义一个谓词词，使得word u w v 成立当且仅当w 是从u 到v 的词。

我有一些定义

type_synonym ('q,'l) lts = "'q ⇒ 'l ⇒ 'q ⇒ bool"

inductive word:: "('q,'l) lts ⇒ 'q ⇒ 'l list ⇒ 'q ⇒ bool" for δ where....

我不明白。

你为什么使用type_synomym 而不仅仅是

inductive word:: " 'q ⇒ 'l list ⇒ 'q ⇒ bool" for δ where....

我的第二个问题是关于 δ 代表什么以及如何表达这种归纳法。是否有任何教程可以用不止一个例子来解释归纳法？

Answer 1

我假设lts 代表标记转换系统。 word 的定义取决于转换系统的特定选择。

您提出的简化类型签名是不够的：如果不指定这是一个词在哪个转换系统中，则提议 word u w v 毫无意义。