Л - не логика, а lua

[amarao]

> nan
nil
> a=0/0
> a
-nan
> a==nill
false
> a==nan
false
> a==-nan
stdin:1: attempt to perform arithmetic on a nil value (global 'nan')
stack traceback:
    stdin:1: in main chunk
    [C]: in ?

После присматривания к результатам... в целом, претензия только к выводу nan как nil.

Comments

[juan_gandhi]

За этим стоит какая-нибудь теория, или это чисто художественная. интерпретация пожеланий инженеров?

[amarao]

Я не знаю какой-то осмысленной теории, но интуиция мне понятна: как только мы получили nan, мы хотим, чтобы все операции дальше везли nan.

С точки зрения логики, мы точно знаем, что 0/0 не равен 0/0. Можно применить иезуитство и сказать, что мы точно знаем, что 0/0 не не равен 0/0, но для практических целей достаточно, что 0/0 != 0/0 (или любая другая такая штука, типа inf - inf).

Задача: выполнить вычисления и не дать ложных результатов.

Для желающих можно включить исключительные ситуации и упасть, но часто бывает, что проще продолжать считать, и просто "poison" результаты. Если оно не расползётся, результаты можно большей частью использовать. Если расползётся, ну, хотя бы мы это знаем.

С точки зрения типов, это что-то типа такого:

Either<f64, poisoned>

причём все poisoned все операции f64 поддерживает, но возвращает poisoned.

Так же poisoned.cmd(poisoned) == False.

Так же:

>>> math.nan < math.nan
False
>>> math.nan > math.nan
False
>>> math.nan >= math.nan
False


и т.д.

[juan_gandhi]

Ну так мы уже в категории Клайсли для монады Option. Either

[Error: Irreparable invalid markup ('<f64,poisoned>') in entry. Owner must fix manually. Raw contents below.]

Ну так мы уже в категории Клайсли для монады Option. Either<f64,poisoned> - это всё равно, что Option<f64>.

[amarao]

!markdown

А вот ты уверен? Прости, я не могу писать угловыми скобками, пусть будут квардратные.

Option[f64] = (Some(f64), None)

poison (он же NaN) => None.

Теперь у нас есть код:

if min_x <= x <= max_x {
...
}

Если у тебя Option, то у тебя None == None, и условие выполняется (если все три nan).

Предположим, в min_x оказалось nan (то есть poison). Инженерный подход - nan сам себе не равен. Так, чтобы если у нас есть такое выражение, то оно было бы false в случае nan на любой позиции.

Option эту проблему не решает.

[juan_gandhi]

В чём проблема? Отменить тотальное равенство для Maybe? Отменить-то можно, а смысл?

someResult match
  case None => println("no result")
  case Some(result) => println(s"Success: $result")

Работать не будет. Вообще интуиционистской логики не построить. Там равенство определяется как классификатор диагонали. Так что нельзя будет определять, например, подобъекты.

В принцпе, NaN нахер не нужен при вычислениях - это сигнал, что результата нет, т.к. функция частичная. Ну, например, кольцо целых чисел не является полем. Ну и чо? На хрена?

[amarao]

Вот Nan - это как раз попытка на ёлку залезть (закончить сложные вычисления) и ничего не ободрать (то есть завершить вычисления, может быть, не до конца испорченные, если nan'ы не сильно расползлись по всем данным).

Бонус: мы видим, какие данные были повреждены, потому что nan'ы заразны (кроме bool'ов, для которых я бы тоже предпочёл poison, но там уже семантика if'ов ползёт). Это всё было придумано практиками, "чтобы считало", а не пришло из теории, насколько я понимаю.

Наверное, где-то есть более формальное и точное описание этой логики (всёж, IEEE стандарт).

Я тут робота послал, он нашёл вот это:

Bagnara, R., Bagnara, A., Biselli, F., Chiari, M. & Gori, R. «Correct Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification». arXiv:1903.06119 (2019).

https://arxiv.org/abs/1903.06119


Brain, M., Tinelli, C., Rümmer, P. & Wahl, T. «An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic». 22nd IEEE Symposium on Computer Arithmetic (ARITH 2015): 160–167.

https://dblp.dagstuhl.de/rec/conf/arith/BrainTRW15.html

Но я это уже понять не могу в силу мощности моего семантического многообразия.

[juan_gandhi]

Я это понимаю как накручивание псевдонауки вокруг неудобного факта, что математики там нет, а есть фантазии прагматиков.

[amarao]

If you say so. А математика там есть, просто не та, которую ты пытаешься построить.

Да, вычисления на float'ах отличаются от тех, которые тебе хотелось бы видеть. Я вот тоже не люблю комплексные числа. И?

-Inf, Inf, -0, +0, Nan - и они образуют интересную структуру, в которой есть делители нуля.

[juan_gandhi]

Я не пытаюсь ничего построить. Но к этим floats было бы неплохо не ad-hoc, а нормальную математику обеспечить.

[amarao]

Так она "нормальная", просто не похожа на мечты математиков о бесконечной гладкости и непрерывности.

[juan_gandhi]

Она формализована? Ассоциативность операций сложения и умножения, например, имеется хотя бы? Если нет, то какой смысл что-то вычислять из, например, аэродинамики?

[yurikhan]

В плавучей арифметике сложение и умножение в общем случае не ассоциативно и без всяких NaN’ов, чисто за счёт ограниченной битности мантиссы. Примерно в духе (2^N + 1) + 1 = 2^N + 1 = 2^N, но 2^N + (1 + 1) = 2^N + 2.

[juan_gandhi]

Да, есть такая проблема; для борьбы с этим есть всякие трюки в вычислительной математики.

Короче да, это не математика, а ближе к химии.

[amarao]

Предложи что-то лучше.

[juan_gandhi]

Я в вычислительной математике не силён.

[amarao]

математики очень любят машину Тьюринга потому что у неё бесконечная лента.

(смотрю в сторону java-отдела, которому в очередной раз подняли лимиты до 300Гб по памяти)