Вопросы по теме 'induction'
доказывая правильность этого рекурсивного алгоритма с помощью индукции
int sumHelper(int n, int a) {
if (n==0) return a;
else return sumHelper(n-1, a + n*n);
}
int sumSqr(int n) {
return sumHelper(n, 0);
}
Ребята, я должен доказать этот фрагмент кода, который использует хвостовую рекурсию для...
257 просмотров
schedule
22.11.2021
Доказательство индукции, что повторение рюкзака возвращает оптимальное решение
Я должен показать по индукции, что
если w ‹w_i, то Opt (i, w) = Opt (i-1, w), иначе Opt (i, w) = max {Opt (i-1, w), Opt (i-1, w - w_i) + w_i)}
дает оптимальное решение задачи о рюкзаке (подход динамического программирования)
Я знаю, как...
631 просмотров
schedule
27.09.2021
доказывая сильную индукцию в coq с нуля
Я занимаюсь доказательством эквивалентности слабой и сильной индукции.
У меня есть такое определение:
Definition strong_induct (nP : nat->Prop) : Prop :=
nP 0 /\
(forall n : nat,
(forall k : nat, k <= n -> nP k) ->
nP (S...
294 просмотров
schedule
10.09.2021
Как доказать a * b * c = a * (b * c) в Coq?
Я пытаюсь доказать поставленный выше вопрос. Мне дали определение индукции:
Definition nat_ind
(p : nat -> Prop)
(basis : p 0)
(step : forall n, p n -> p (S n)) :
forall n, p n := fix f n :=
match n return p n with
|...
66 просмотров
schedule
14.10.2021
Индуктивная лемма Дафни: нельзя вывести постусловие индукционной гипотезы
Я пытаюсь определить семантику малых шагов очень простого языка с помощью арифметических выражений (исходный код доступен здесь ). Для простоты мы предполагаем, что язык допускает только литералы и унарный минус ( -exp ).
datatype expression =...
83 просмотров
schedule
24.02.2022
Введение в алгоритмы, третье издание. Упражнение 2.3.3. Индуктивное доказательство nlg(n)
Я читаю книгу «Введение в алгоритмы», третье издание. В упражнении нас просят использовать индуктивное рассуждение, чтобы доказать
T(n) = {2 if n = 2, 2T(n/2) + n if n > 2^k for k > 1} = nlgn
Где lg - логарифмическая база 2. В книге...
486 просмотров
schedule
25.02.2022
Используя Omega для доказательства леммы в Coq
Я пытаюсь сделать доказательство в Coq с помощью Omega. Я потратил на это много времени, но мне ничего не пришло. Я должен сказать, что я новичок в Coq, поэтому мне не нравится этот язык, и у меня нет большого опыта. Но я работаю над этим.
Вот...
803 просмотров
schedule
22.03.2022
Доказательство OCaml методом структурной индукции
Учитывая следующую функцию:
let rec foo l1 l2 =
match (l1,l2) with
([],ys) -> ys
| (x::xs,ys) -> foo xs (x::ys))
Докажите следующее свойство:
foo (foo xs ys) zs = foo ys (xs@zs)
Пока что я завершил базовый...
408 просмотров
schedule
27.03.2022
Доказательство индукции $T(n) = 9T(n/3) + n^2$
Как я могу доказать, что повторение
Т(n) = 9T(n/3) + n 2
приводит к T(n) = O(n 2 log(n)) с использованием метода подстановки и доказательства по индукции? Мне не разрешено использовать основную теорему.
Используя индукцию и...
2475 просмотров
schedule
28.03.2022
Как доказать правильность этого алгоритма?
Мой алгоритм: построить новый граф G', тогда как для каждой вершины v в V создать две вершины v_0 и v_1 в G', и для каждого ребра (u, v) в E, создайте два ребра (u_0, v_1) и (u_1,v_0) в G'. Запустите Dijkstra на G', начиная с s_0.
Все пути в G',...
149 просмотров
schedule
28.03.2022
Доказательство через количество шагов вывода
Даны G = {a, b, c, d}, {S, X, Y}, S, {S->XY, X->aXb, X->ab, Y->cYd, Y->cY, Y ->кд}}
Докажите, что |w|c-|w|d+|w|a≥|w|b
|w|a — это количество букв «a» в строке. Это имеет смысл, так как будет больше (или такое же количество) 'c', чем 'd',...
55 просмотров
schedule
26.04.2022
Завершение леммы о списке нац
Я вынужден доказать следующую признанную лемму. Пожалуйста, помогите мне, как действовать.
Функция sumoneseq добавляет и возвращает список повторений "истина" в обратном порядке. Если задано [ true ; false; true; true ; false; true; true;...
82 просмотров
schedule
14.05.2022
Доказательство структурной индукции на объединении IntSet
Предположим, у вас есть следующее определение:
abstract class IntSet {
def incl(x: Int): IntSet
def contains(x: Int): Boolean
def union(other: IntSet): IntSet
}
case class NonEmpty(elem: Int, left: IntSet, right: IntSet) extends...
222 просмотров
schedule
20.05.2022
Coq: Как сформулировать сильную гипотезу полиморфного зависимого типа
У меня были проблемы с зависимой индукцией из-за «слабой гипотезы».
Например :
У меня есть зависимый полный складной список:
Inductive list (A : Type) (f : A -> A -> A) : A -> Type :=
|Acons : forall {x x'' : A} (y' : A) (cons' :...
97 просмотров
schedule
26.05.2022
Докажите, что rev (rev l) = l в Coq
Это одно из упражнений, данных мне, я застрял почти сразу после индукции по l. Я не знаю, какое еще утверждение здесь можно сделать.
Мне не разрешено использовать сложные тактики, такие как авто, интуиция и т. Д.
Fixpoint snoc {A : Type} l a :...
243 просмотров
schedule
30.05.2022
Как мне написать собственное правило индукции для параметризованного индуктивного набора?
Я пытаюсь написать собственное правило индукции для индуктивного набора. К сожалению, когда я пытаюсь применить это с induction rule: my_induct_rule , я получаю лишнее, невозможно доказать. Имею следующее:
inductive iterate :: "('a ⇒ 'a ⇒ bool)...
200 просмотров
schedule
21.06.2022
Перестановки векторов Coq
Мне нужно рассуждать о перестановках векторов в Coq. Стандартная библиотека включает только определения перестановок для списков. В качестве первой попытки я попытался имитировать это для векторов как:
Inductive VPermutation: forall n, vector...
226 просмотров
schedule
26.06.2022
Как мне доказать, что elem z (xs ++ ys) == elem z xs || элем з ыс?
У меня есть следующее:
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
Я попытался сделать...
323 просмотров
schedule
15.08.2022
TWISTED Самая длинная общая подпоследовательность
Меня интересовал особый случай проблемы самой длинной общей подпоследовательности http://en.wikipedia.org/wiki/Longest_common_subsequence_problem Что, если у нас есть две строки из n символов, и гарантируется, что обе они содержат ровно 1 символ и...
187 просмотров
schedule
27.08.2022
Дафни и подсчет вхождений
Я смотрел на использование лемм в Дафни, но мне трудно понять, и, очевидно, приведенный ниже пример не подтверждается, вполне возможно, потому, что Дафни не видит индукции или что-то вроде леммы, чтобы доказать какое-то свойство count ? По сути, я...
818 просмотров
schedule
29.08.2022
