Описание тега induction
Все, что связано с принципом математической индукции и методами, применяемыми в вычислениях. НЕ ИСПОЛЬЗУЙТЕ этот тег для вопросов, связанных только с математикой, поскольку они не относятся к теме SO. Этот тег можно использовать для вопросов, связанных с математикой, только если он связан с некоторыми действиями по программированию или программными инструментами (например, автоматическое доказательство теорем и т. Д.).
1
ответ
Введение в алгоритмы Третье издание - Упражнение 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. Книга предлагает решение: Bas…
07 июл '15 в 04:21
1
ответ
Когда пространство гипотезы содержит целевую концепцию
Что это означает, когда написано, что пространство гипотез содержит целевое понятие? Если возможно с примером.
04 сен '16 в 13:59
1
ответ
Какие размеры в Агде?
Какие размеры в Агде? Я пытался прочитать статью о MiniAgda, но не смог продолжить из-за следующих моментов: Почему типы данных являются общими для их размера? Насколько я знаю, размер - это глубина дерева индукции. Почему типы данных ковариантны от…
02 ноя '16 в 15:27
3
ответа
Являются ли списки индуктивными или индуктивными в Хаскеле?
Так что в последнее время я читаю о коиндукции, и теперь мне интересно: списки на Haskell индуктивны или коиндуктивны? Я также слышал, что Хаскелл не различает их, но если да, то как они делают это формально? Списки определяются индуктивно, data [a]…
04 окт '16 в 14:09
1
ответ
Доказательство структурной индукции на объединении 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 IntSet { def incl(x:…
08 июл '16 в 10:59
1
ответ
Доказательство того, что бинарное дерево с n листьями имеет высоту не менее log n
Мне удалось создать доказательство, которое показывает, что максимальное количество узлов в дереве равно n = 2^(h+1) - 1, и логически я знаю, что высота двоичного дерева равна log n (могу нарисовать его) чтобы увидеть) но у меня возникли проблемы с …
22 авг '17 в 12:16
1
ответ
Математические доказательства индукции
Для моей теории теории вычислений, мы должны решить некоторые проблемы с обзором / практикой, чтобы избавиться от ржавчины и убедиться, что мы готовы к курсу. Некоторые из проблем являются индукционными доказательствами. Я сделал это в свое время, н…
10 сен '13 в 22:34
2
ответа
Принцип индукции, генерируемый Coq, ведет себя не так, как я хочу
Отредактировано для понятности Я пытаюсь доказать свойства дерева особого типа. Это дерево похоже на следующее. Проблема в том, что принцип индукции, сгенерированный Coq, недостаточен для доказательства свойств дерева. Для более простого примера, ск…
10 фев '16 в 12:40
1
ответ
Как применить индуктивное мышление к `GHC.TypeLits.Nat`?
Рассмотрим это определение zip для обычной длины векторов, индексируемых цифрами Пеано: {-# language DataKinds #-} {-# language KindSignatures #-} {-# language GADTs #-} {-# language TypeOperators #-} {-# language StandaloneDeriving #-} {-# language…
19 авг '18 в 12:11
1
ответ
Доказательство правильности алгоритма по индукции
Недавно я начал читать книгу о структурах данных, и она начинается с введения в алгоритмы. В одном упражнении он просит доказать алгоритм по индукции и инвариант цикла. Алгоритм в псевдокоде: Algorithm DEC2BIN(int n, int[] b) Input: int n, array b O…
17 июн '18 в 12:01
1
ответ
Индуктивная лемма Дафни: не может вывести постусловие индукционной гипотезы
Я пытаюсь определить семантику маленького шага очень простого языка с помощью арифметических выражений (исходный код доступен здесь). Для простоты мы предполагаем, что язык допускает только литералы и унарный минус (-exp). datatype expression = Lite…
08 июн '18 в 20:04
2
ответа
Как доказать в Coq утверждения о заданных множествах
Как одно доказательство утверждения, как следующее в COQ. Require Import Vector. Import VectorNotations. Require Import Fin. Definition v:=[1;2;3;4;5;6;7;8]. Lemma L: forall (x: Fin.t 8), (nth v x) > 0. Или, скажем, у вас есть заданный список чис…
19 дек '15 в 19:39
1
ответ
Coq индукционный старт на определенном нат
Я пытаюсь изучить coq, поэтому, пожалуйста, предположите, что я ничего не знаю об этом. Если у меня есть лемма в coq, которая начинается forall n m:nat, n>=1 -> m>=1 ... И я хочу продолжить по индукции по n. Как начать индукцию с 1? В насто…
29 ноя '14 в 18:34
2
ответа
Доказательство введением псевдокода
Я не очень понимаю, как использовать доказательство по индукции на psuedocode. Кажется, это не работает так же, как использование его в математических уравнениях. Я пытаюсь подсчитать количество целых чисел, которые делятся на k в массиве. Algorithm…
08 окт '11 в 20:49
1
ответ
Может ли кто-нибудь предоставить мне лучшее доказательство и сценарий для пузырьковой сортировки по сравнению с тем, что я доказал?
Дайте список несортированных элементов. Начальное условие: A= список несортированных элементов, p=1, N= общий размер массива. Bubble(A,p,N) if p>=N return for i=p to N-1 if A[i]>A[i+1] swap(A[i],A[i+1]) Bubble(A,p,N-1) Вопрос 1: Докажите прави…
18 июл '17 в 15:21
2
ответа
Как настроить индуктивное доказательство в haskell?
Мне нужно доказать f (g xs) == g (f xs) всякий раз, когда xs является конечным списком Ints. Предположим, что f и g имеют тип [Int]->[Int]
24 апр '17 в 22:44
1
ответ
Coq - индукция в списках с функцией, примененной к каждому элементу
Пытаюсь доказать, что применение функции f к каждому элементу из двух списков приводит к аналогичным rel_list списки, если они были первоначально связаны. у меня есть rel на элементы списка и доказали лемму Lemma1 что если два элемента находятся в r…
18 дек '13 в 17:44
1
ответ
Что такое индуктивно определенный тип данных?
Какие примеры индуктивных типов данных? Чем индуктивные типы отличаются от неиндуктивных аналогов? Что они могут сделать, что иначе невозможно? Когда их не следует использовать? Фрагменты кода на любом языке будут с благодарностью.
02 май '18 в 22:19
1
ответ
Какова интуиция за шахматной доской, охватывающей рекурсивный алгоритм, и как можно лучше сформулировать такой алгоритм?
Возможно, вы слышали о классической головоломке с шахматной доской. Как вы покрываете шахматную доску, у которой отсутствует один угловой квадрат, используя L-образные плитки? Существует рекурсивный подход к этому, как объяснено в книге "Освоение ос…
23 май '15 в 16:24
1
ответ
Рассчитать количество узлов из числа дуг в дереве - Индукция
Если дерево имеет k дуг, сколько у него узлов? Базовый вариант: If k=0 => n=(k+1)=1 Индуктивная гипотеза: For every k, n=(k+1) is true Доказательство: Is it true for k=1? k=n-1 1=n-1 1=(k+1)-1 k=1,so: 1=1+1-1 1=1 Proved? Я что-то пропустил?
03 апр '17 в 10:01