我有以下内容:
elem :: Eq a => a -> [a] -> Bool
elem _ [] = False
elem x (y:ys) = x == y || elem x ys
我怎样才能证明所有x的y和z都是......
elem z (xs ++ ys) == elem z xs || elem z ys
我试图让左侧等同于右侧,但我的尝试都没有取得丰硕成果.
L.S elem z (x:xs ++ y:ys) = z==x || z==y || elem xs || elem ys
R.S elem z (x:xs) || elem z (y:ys) = z==x || z==y || elem xs || elem ys
有人可以帮我吗？
data Nat = Zero | Succ Nat
type Predicate = (Nat -> Bool)
-- forAllNat p = (p n) for every finite defined n :: Nat
implies :: Bool -> Bool -> Bool
implies p q = (not p) || q
basecase :: Predicate -> Bool
basecase p = p Zero
jump :: Predicate -> Predicate
jump p n = implies (p n) (p (Succ n))
indstep :: Predicate -> Bool
indstep p = forallnat (jump p)
题:
证明如果basecase …
我一直在玩归纳类型（定义的自然数和对它们的算术运算），但我无法让 Haskell 读取函数工作。
这是我的代码：
data Natural = Zero | Succ Natural
deriving (Eq, Ord)
instance Enum Natural where
pred Zero = undefined
pred (Succ x) = x
succ x = Succ x
toEnum 0 = Zero
toEnum x = Succ (toEnum (x - 1))
fromEnum Zero = 0
fromEnum (Succ x) = fromEnum x + 1
instance Num Natural where
(+) x Zero = x
(+) x (Succ y) = Succ (x + y)
(-) Zero (Succ x) = undefined …我有一个计算机程序,读取一个字符数组,操作数和运算符用后缀表示法编写.然后程序扫描数组,通过使用堆栈计算结果,如下所示:
get next char in array until there are no more
if char is operand
push operand into stack
if char is operator
a = pop from stack
b = pop from stack
perform operation using a and b as arguments
push result
result = pop from stack
如何通过归纳证明此程序正确评估任何后缀表达式？(摘自练习4.16 Java中的算法(Sedgewick 2003))
我有充分理解如何证明以下某些陈述的问题.
例如,我有一个声明:n^2logn = O(n^2).纠正我,如果我错了,但这个规定,n^2是bigO的n^2logn.意味着n^2增长得快于n^2logn.现在我们将如何证明这一点？我假设我需要使用感应证明,我试图使用但是在这个过程中卡住了.我可以重写这句话n^2logn <= n^2吗？
是否有可能使用归纳法反驳某些东西？例如,反驳n!=O(n^n).或者通过简单地表明任意值(例如大于2)不满足该陈述来反驳该陈述是否有效？
最后为了清楚起见,bigTheta声明方程式在增长正确时是等价的？
鉴于这两个功能:
sumOne 0 = 0 -- I.a
sumOne m | m > 0 = sumOne (m-1) + m -- II.a
endSum m = helpSum 0 m -- I.b
where helpSum x 0 = x -- II.b
helpSum x m | m > 0 = helpSum (x+m) (m-1) -- III.b
我们必须通过归纳证明sumOne = endSum.
所以我尝试过:
对于 n=0
sumOne 0=0 == endSum 0 = helpSum 0 0 = 0 True
假设:
sumOne m + k = helpSumm k m
诱导步骤:
-> m=m+1
helpSum …我坚持要证明以下公认的引理。请帮助我如何继续。
函数sumoneseq以相反的顺序添加并返回“true”的重复列表。鉴于 [真;假; 真;真;假; true;true;true ]，它返回 [3;2;1]。该功能sumones在NAT表增加值。给定 [3;2;1]，它返回 6。
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Fixpoint sumoneseq (lb: list bool) (ln: list nat) : list nat :=
match lb, ln with
| nil, 0::tl'' => tl''
| nil, _ => ln
| true::tl', nil => …我想知道如何在结构归纳法中显示列出 xs ，或者归纳法如何工作：
map f (map g xs) = map (\x -> f(g x)) xs
通过这个函数定义
map :: ( a -> b ) -> [ a ] -> [ b ]
map _ [] = []
map f ( x : xs ) = f x : map f xs
是不是像数学归纳法一样？
提前致谢
我需要证明
f (g xs) == g (f xs)
当 xs 是 Int 的有限列表时。
假设 f 和 g 都是 [Int]->[Int] 类型
在算法设计手册（第16页）一书中，讨论了以下增量算法的正确性的归纳证明。
Increment(y)
if (y == 0) return 1;
else if (y % 2 == 1) return 2 * Increment(floor(y/2));
else return y + 1;
但我在讨论中的某一点（或假设）感到困惑。请求解决方案（通过归纳证明正确性）以更好地理解。