mk строит дерево высотой n (==) выполняет поэлементное сравнение значений, не пытаясь сократить до сравнения адресов. Ну, как бы, логично получить такой эффект. Постулируется, что `x == x` для любых значений любых типов? Даже если рукожопо определить инстанс тайпкласса Eq? А если сравнивать бесконечные списки? let xs = [1..] in xs == xs, то вообще всё будет ужасно?
Ну и вопрос, а есть ли - и могут ли вообще быть - ленивые языки, которые пригодны к вот таким символьным вычислениям? Ведь, даже если мы строим пышное дерево, вырожденное до вот такого списка, то можем сделать так, чтобы ленивые санки там были разные. let x = mk (n-1) in let y _ = x in P (y 1) (y 2)
А, я понял. Это я стормозил. Мы тут сравниваем не идентичные объекты, - санки и структуры с разными адресами. Проблему можно было бы полечить, если бы мы умели кэшировать результаты сравнения.
a = mk 3 a = T {@1= {T @2= {T @3=V ; @3} ; @2} ; @1}
b = mk 3 a = T {@4= {T @5= {T @6=V ; @6} ; @5} ; @4}
a == b = @1 == @4 = @3 == @5 = @4 == @6 = V == V = True && @4 == @6 = True из кеша && @3 == @5 = True из кеша && @1 == @4 = True из кеша = True
Но понятно, что кеш не резиновый. Найдётся способ его прострелить, и у нас сравнение будет линейно-линейно-линейно-... БАБАХ экспоненциально Либо же мы резиновый кеш должны таскать с собой неопределённо долго, и это будет ещё один способ утечки памяти.
Да, насыщение равенствами должно быть реализовано через hash consing, и никак иначе, и, поэтому, структурное равенство двух значений может быть вычислено непосредственно за O(1).
Comments 22
(==) выполняет поэлементное сравнение значений, не пытаясь сократить до сравнения адресов. Ну, как бы, логично получить такой эффект.
Постулируется, что `x == x` для любых значений любых типов? Даже если рукожопо определить инстанс тайпкласса Eq?
А если сравнивать бесконечные списки? let xs = [1..] in xs == xs, то вообще всё будет ужасно?
Ну и вопрос, а есть ли - и могут ли вообще быть - ленивые языки, которые пригодны к вот таким символьным вычислениям?
Ведь, даже если мы строим пышное дерево, вырожденное до вот такого списка, то можем сделать так, чтобы ленивые санки там были разные.
let x = mk (n-1) in let y _ = x in P (y 1) (y 2)
Reply
let xs = [1..] in xs == xs технически может сравнить санки (их адрес), разве нет?
Reply
Технически может сравнить санки, но для этого нужны гарантии аксиоматики операции сравнения.
Обычно из идентичности следует равенство, но вот в си, например, float NaN не равен сам себе.
Ну и какой-нибудь злобный дурак может устроить wish you happy debug, определив для своего типа равенство хаотичным способом
Reply
Они есть в случае Хаскеля.
Reply
Проблему можно было бы полечить, если бы мы умели кэшировать результаты сравнения.
a = mk 3
a = T {@1= {T @2= {T @3=V ; @3} ; @2} ; @1}
b = mk 3
a = T {@4= {T @5= {T @6=V ; @6} ; @5} ; @4}
a == b =
@1 == @4 =
@3 == @5 =
@4 == @6 =
V == V = True
&& @4 == @6 = True из кеша
&& @3 == @5 = True из кеша
&& @1 == @4 = True из кеша
= True
Но понятно, что кеш не резиновый. Найдётся способ его прострелить, и у нас сравнение будет линейно-линейно-линейно-... БАБАХ экспоненциально
Либо же мы резиновый кеш должны таскать с собой неопределённо долго, и это будет ещё один способ утечки памяти.
Reply
(ведь насыщение равенствами https://rosstate.org/publications/eqsat/ Тьюринг-полно)
Сборка мусора будет интересным занятием. ;)
Да, насыщение равенствами должно быть реализовано через hash consing, и никак иначе, и, поэтому, структурное равенство двух значений может быть вычислено непосредственно за O(1).
Reply
Leave a comment