Об умножение

[deniok]

Эти ваши интернеты бурлят:

ru-marazm.livejournal.com/3591670.html

lj.rossia.org/users/tiphareth/1685303.html

Агда, кстати, на стороне внучки, 9 раз по 2 литра будет 9 * 2:

_*_ : ℕ → ℕ → ℕ
zero  * n = zero
suc m * n = n + (m * n)

Впрочем внучке стоило бы снять все вопросы, предоставив доказательство

*-commutative : ∀ m n → m * n ≡ n * m

Взяв его, например, из Data.Nat.Properties. Или получив самостоятельно.

Comments

[sassa_nf]

А я получаю вот такое:

An internal error has occurred. Please report this as a bug.
Location of the error: src/full\Agda\Interaction\GhciTop.hs:646

Это вообще известно как бороть?

(C-c C-l в емаксе)

[deniok]

Модуль, например, не надо называть Test :)
(это я описываю тот случай, когда получал нечто подобное)

[sassa_nf]

хахаха, :) файл на виндовз начинался с маленькой буквы. Вышел из емакса, переименовал с большой буквой - все дела :)

[thedeemon.livejournal.com]

Значит, следует во втором классе сперва обучать Агде, а потом уже задачи на умножение решать. :)

[deni-ok.livejournal.com]

Умножение в младших классах вводится как не очень симметричная операция: повторить сложение числа с собой несколько раз. И сначала имеет смысл прочувствовать как устроены 2+2+2+2+2+2+2+2+2 и 9+9. Затем удивиться, что получается одно и то же число 18. Ну а только потом переходить к коммутативности вращением прямоугольной упаковки: 2 рада по 9 предметов превращаются в 9 рядов по 2 предмета.

Так что, независимо от Агды, после первого этапа какая-то конвенция имеет смысл. Временный, конечно, что и порождает лютую дискуссию.

[nivanych.livejournal.com]

Ну вот! Практическое использование, самое, что ни на есть!

[thedeemon.livejournal.com]

умножения? :)

[nivanych.livejournal.com]

Агды!
А как ещё докажешь учителю правоту?

[nealar.livejournal.com]

Ты же сам рассказывал про нунчаки с цепочкой от собаки!

[deni-ok.livejournal.com]

Эта система доказательств полна и непротиворечива. Слишком мощно для наших целей!

[nivanych.livejournal.com]

Нунчаки, это overkill!

[nealar.livejournal.com]

Полна и противоречива, скорей.

[deni-ok.livejournal.com]

Противоречьями полна
Нас не устроила она.

[nivanych.livejournal.com]

Йа не готов сидеть.
А так ничо, да — полна и непротиворечива ;-)

[thedeemon.livejournal.com]

Сомневаюсь, что учитель примет доказательство на Агде. Скорее всего, потребует на Coq.

[nivanych.livejournal.com]

Ох уж эти традиции французской школы!

[thedeemon.livejournal.com]

Oui, monsieur. Скажет, таковы требования Gauronault.

[deni-ok.livejournal.com]

Ну это если франкофон, то да.

[helvegr.livejournal.com]

F# с units of measure:

// Volume, liters.
[<Measure>] type L

let answer1 = 9 * 2<L>
let answer2 = 2<L> * 9

>
[<Measure>]
type L
val answer1 : int<L> = 18
val answer2 : int<L> = 18

То же самое, если ввести единицу измерения "литропокупатель".