но каждый шаг рекурсии - не частичный
ну я понял, короче ей нельзя подсунуть аргумент, который она не может заматчить? это твоё определение?
Ilya
Ilya
или как
Aleksei (astynax)
> ей нельзя подсунуть аргумент, который она не может заматчить
да
Aleksei (astynax)
в отличие от head, например
Aleksei (astynax)
рекурсивная функция, которая тупо зацикливается - частично определена?
она по построению не возвращает результат :)
Ilya
head2 :: [a] -> a
head2 (x:xs) = x
head2 [] = head2 []
Ilya
head2 частичная или нет?
Aleksei (astynax)
Тут рекурсия без убывания аргумента. Это просто ошибка программиста :)
Алексей
Так тотальноть не про ошибки программиста
Aleksei (astynax)
У length аргумент убывает. Если аргумент конечен, то результат всегда будет.
Алексей
Length тотальна для клнечных списков
Ilya
Тут рекурсия без убывания аргумента. Это просто ошибка программиста :)
ну так ты дал определение, head2 под него подходит, значит всё ок
Ilya
или снова меняем определение, я не против
Aleksei (astynax)
Я не давал определение ещё
Aleksei (astynax)
Соответственно я его и не меняю
Aleksei (astynax)
Меня устраивает опредедение из вики
Aleksei (astynax)
Считать ли некорректно написанные рукурсивный функции частичными или нет - вопрос
Алексей ayaye :)
Считать ли некорректно написанные рукурсивный функции частичными или нет - вопрос
особенно если учесть существование проблемы останова )
Алексей
Что значит некорректно написанные функции?
Alexander
у нас там проблема останова решена?
Alexander
чтобы length тотальной сделать?
Aleksei (astynax)
При этом в хаскеле из за ленивости вполне можно писать полезные "неправильно рекурсивные" функции :)
ones = 1 : ones
Алексей ayaye :)
f 1 = 1
f n | even n = f(n / 2)
| otherwise = f (3*n+1)
полностью определена?
Ilya
При этом в хаскеле из за ленивости вполне можно писать полезные "неправильно рекурсивные" функции :)
ones = 1 : ones
а вот это как раз не частичная функция, внезапно
Alexander
f 1 = 1
f n | even n = f(n / 2)
| otherwise = f (3*n+1)
полностью определена?
забыл рекурсию или базовый случай?
Cheese
Окей, что мы даём на вход и ожидаем на выходе? можно считать по NF, length тотальная. по WHNF length частичная
Aleksei (astynax)
а вот это как раз не частичная функция, внезапно
А я и не сказал, что она частичная нигде. Я сказал, что она "некорректно рекурсивная" :)
Ilya
"некорректно рекурсивная" корекурсивная что ль
Ilya
потому ones корекурсивна
Aleksei (astynax)
"нет базового случая и аргумент не убывает"
Алексей ayaye :)
полностью определена?
Алексей ayaye :)
f 1 = 1
f n | even n = f(n / 2)
| otherwise = f (3*n+1)
полностью определена?
Aleksei (astynax)
Останов не гарантируется, все значения аргумента будут обработаны
Cheese
Останов не гарантируется, все значения аргумента будут обработаны
что значит "обработаны" и зачем это вообще?
Aleksei (astynax)
что было
Vladimir
чтобы length тотальной сделать?
Будто нерешённая проблема останова мешает определить множество частичных функций по завершаемости вычисления. Ну не будет задача определения тотальности разрешимой алгоритмом, и чо из этого?
Alexander
конечно мешает, посмотри на coq или агду и насколько много функций тотальность которых они не могут доказать
Danila Matveev
Будто нерешённая проблема останова мешает определить множество частичных функций по завершаемости вычисления. Ну не будет задача определения тотальности разрешимой алгоритмом, и чо из этого?
не распарсил текст %)
но про останов писали уже, это необходимое условие для тотальности
Алексей
Определить множество ничего не мешает. Оно будет невычислимым, ну и ладно
Alexander
доказательства уровня "чем-нибудь клянусь" это не круто
Aleksei (astynax)
repeat - частичная?
Aleksei (astynax)
никогда не остановится
Alexander
ну она возвращает WHNF сразу и на всех входах
Alexander
вообще с кодатой все всегда весело
Cheese
не распарсил текст %)
но про останов писали уже, это необходимое условие для тотальности
да, но вычисление останавливаемости мешает вычислять тотальность
Alexander
особенно никогда она одновременно и кодата и дата
Danila Matveev
да, но вычисление останавливаемости мешает вычислять тотальность
это уже что-то про (автоматическое?) доказательство
вопрос все же был что есть тотальная и частичная
Cheese
в общем, length на WHNF (1 : ones) не даёт результат в WHNF. @astynax неправ
Danila Matveev
это уже что-то про (автоматическое?) доказательство
вопрос все же был что есть тотальная и частичная
и надо все же разделять классическую мат функцию и то что в яп (какой-нить более специфичной математики), потому что в первом случае нет понятия о длительности вычисления, результат либо существует, либо нет
Cheese
можно сказать, что length — «функция с полным определением» (кстати, это называется total в Liquid Haskell)
Cheese
и надо все же разделять классическую мат функцию и то что в яп (какой-нить более специфичной математики), потому что в первом случае нет понятия о длительности вычисления, результат либо существует, либо нет
тезис Чёрча—Тьюринга говорит, что не надо разделять
Alexander
totalLength c !p [] = Right (p+c)
totalLength c p (_:xs)
| p < chunkSize = totalLength c (p+1) xs
| otherwise = Left $ \() -> totalLength (c+p) 0 xs
Alexander
(писал с тапка)
Alexander
удобно бы было работать?
Евгений
length определена на всех значениях аргумента
Ты под значениями только конструкторы понимаешь? Такое. Всё-таки значения -- это набор термов, удовлетворяющих данному типу
Aleksei (astynax)
оке, был неправ - в первый раз что ли :)
Aleksei (astynax)
Ilya
Вопрос: а обилие частично определённых функций в стандартной библиотеке хаскеля это баг или фича?
а теперь можно и на исходный вопрос ответить
"обилие частично определённых функций в стандартной библиотеке хаскеля" — это, несомненно, фича
Danila Matveev
тезис Чёрча—Тьюринга говорит, что не надо разделять
этот тезис как раз подразумевает существование понятия вычислимость (если верить вики), чего нет в определении функции математической
саша
а теперь можно и на исходный вопрос ответить
"обилие частично определённых функций в стандартной библиотеке хаскеля" — это, несомненно, фича
так, а если теперь забыть о length и прочих свёртках бесконечных списков?
Ilya
так, а если теперь забыть о length и прочих свёртках бесконечных списков?
Я за то, что всё ещё фича
Ilya
Но лучше конкретные функции обсуждать, чем судить в целом
Ilya
Какие-то полезны своей частичностью, какие-то нет
Евгений
Нельзя сказать, что частичность это фича. Частичность это неизбежность, если внутри языка нет пруф-асистент подмножества, явно разделяющего тотальное и нетотальное
Ilya
Нельзя сказать, что частичность это фича. Частичность это неизбежность, если внутри языка нет пруф-асистент подмножества, явно разделяющего тотальное и нетотальное
Явно разделяющего точно тотальное и возможно нетотальное
саша
Ну в общем моя претензия в блахе изначально была к тому, что такие функции как head, (!!), read, tail, etc выбрасывают ексепшн, вместо того, чтобы возвращать Maybe/Either
Ilya
Так-то ты прав конечно, про неизбежность
саша
Я тут именно про дизайн библиотеки
Ilya
Ну в общем моя претензия в блахе изначально была к тому, что такие функции как head, (!!), read, tail, etc выбрасывают ексепшн, вместо того, чтобы возвращать Maybe/Either
uncons и readMaybe есть, а если ты уверен, что они не понадобятся -- для тех случаев и head с read
Евгений
Явно разделяющего точно тотальное и возможно нетотальное
Не очень корректно написал. Конечно возможно нетотальное
Aleksei (astynax)
Aleksei (astynax)
Библиотеки типа safe и сторонние прелюдии - вот это всё
Ilya
в Хаскелле всегда можно говорить про тотальность только с оговорками, иначе у нас тотальными только id, const и подобные будут, из-за боттомов в каждом типе
Ilya
Отличная функция id