0 

inductive S :: "alpha list ⇒ bool" where
 empty : "S []" | 
 step1 : "S w ⟹ S (a # w @ [b])" |
 step2 : "⟦S w1; S w2⟧ ⟹ S (w1 @ w2)"

inductive T :: "alpha list ⇒ bool" where
 empty : "T []" |
 step : "⟦T w1; T w2⟧ ⟹ T (w1 @ [a] @ w2 @ [b])"

fun balanced :: "nat ⇒ alpha list ⇒ bool" where
"balanced 0 w = S w"  |
"balanced (Suc 0) w = S (a # w)" |
"(balanced n w = S (a # m @ w)) ⟹ (balanced (Suc n) w = S (a # a # m @ w))"

我正在尝试编写一个函数balanced，以便balanced n w当且仅当S (an @ w)列表包含n相同字母列表的数量时才是正确的。对于函数的第三个方程，"(balanced n w = S (a # m @ w)) ⟹ (balanced (Suc n) w = S (a # a # m @ w))"我得到错误“变量“m”仅出现在右侧：”即使m左侧有。我能想到的唯一解决方案是以另一种方式编写函数，但目前无法想到如何。

4

1 回答 1

0

就目前而言，您的定义没有多大意义。您试图m从 的结果中找出来balanced n w，即使返回的类型是 a bool。你不能把它变成传递给的具体参数，S就像你不能把肉切碎成会走路的鸡一样。

如果你真的想说“如果有一些m满足这个，那么就使用那个m”，那么你需要一个明确的存在量词，然后将你的手放在见证人身上，作为与SOME运算符的实际表达。不过，我不建议这样做。

我相信你实际上想说的是balanced n w = S (replicate n a @ w)。这个定义被接受没有问题（如果我记得正确的参数顺序replicate），但是对于证明这两个语法等价的潜​​在问题，这个定义对你没有帮助。

在这个证明中引入balanced中间概念的目的是您不必直接将派生树映射到另一棵派生树。你真正想要的是一个函数，它w递归地处理输入，从左到右，并且不引用任何一个S或根本不引用T。换句话说，您需要一种算法来决定语法是否与输入匹配。balanced n w = S (replicate n a @ w)那么通过归纳来证明它是一件好事。

由于这是一个练习（来自 prog-prove 和/或具体语义，如果有人在家的话），我现在不会只向您展示递归定义，但如果您在尝试得到它时遇到困难，请告诉我去工作。

于 2021-07-22T12:33:22.667 回答