λ
что умножение с нулем это ноль
то есть
forall (x :: Int) . x * 0 = 0 /\ 0 * x = 0?forall (x :: Int) . x * 0 = 0 /\ 0 * x = 0?Size: a a a
2019 December 25
AZ
то есть
я выше написал примерно
p
очень за тебя рад. А я постоянно так делаю
А что там нужно было сделать? Я практически никогда так напрямую не присваивал значение полю структуры.
С
Да. Кроме io, числодробилок, и web-серверов (выше писал, что в питоне есть для этого)
И текстового редактора с проверкой орфографии и грамматики.
AZ
А что там нужно было сделать? Я практически никогда так напрямую не присваивал значение полю структуры.
по-моему там был пересчет координат снежинок
AZ
но потом добавили снежинки другого вида у которых координаты x не было
λ
я выше написал примерно
короче, индукция — это способ доказательства, а перед доказательством тебе надо сформулировать теорему
AZ
короче, индукция — это способ доказательства, а перед доказательством тебе надо сформулировать теорему
какую теорему доказывает факториал?
p
И текстового редактора с проверкой орфографии и грамматики.
Хз, текстовый редактор на питоне такое. Основная его сфера это веб и прототипирование.
λ
какую теорему доказывает факториал?
эм, факториал ничего не доказывает
p
Некоторые извращенцы используют для администрирования его
AZ
эм, факториал ничего не доказывает
но гарри-ковард, любая программа что-то доказывает
λ
но допустим мы хотим написать эффективную хвосторекурсивную реализацию и хотим доказать её правильность, тогда мы будем доказывать, что результат эталонной функции равен эффективной
λ
но гарри-ковард, любая программа что-то доказывает
ну тогда она доказывает, что из Nat выводится Nat
λ
в целом, для этого хватило бы
idAZ
Всё верно, но модель не всегда есть
AZ
ну тогда она доказывает, что из Nat выводится Nat
нет, это разные утверждения
AZ
я бы сказал что доказывает что существуют числа такие что
AZ
f(x) = f(x-1)*x
λ
нет, это разные утверждения
fib :: Nat -> Nat, (->) это интуиционистская импликация