История изменений

В смысле? Оно запустит для всех k от 1 до 100000000000 при компиляции?

я думаю ты уже выяснил этот момент для себя, всё таки для ясности отвечу: нет, оно просто завершит функцию по достижению переданного числа шагов, если заворачивать в монаду.

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

Есть другие способы. Можно доказать что функция завершается и передать это доказательство Коку в аргументе определяемой функции.

Я может попробую изобразить на досуге, но я этим не занимался, вероятно займёт какое-то время.

И я ещё обещался написать про мьютексы.

Честно говоря задачка про мьютексы не выглядит интересной для меня, поскольку там точно всё получится. Я подобное писал вот здесь https://github.com/andreykl/crosses-zeros/blob/master/Lib.idr (когда читал книжку Бреди про Идрис, там прекрасные примеры). Тут надо смотреть на тип GameCmd который обеспечивает переход игры из одного состояния в другое и при попытке перейти не вовремя, будет ошибка времени компиляции. Ну собственно этот код взять и переписать чуток да и всё.

Но эта задачка выглядит интересной с точки зрения показать: там легко всё понять в самой постановке задачи (последовательность из n-мьютексов это как бы не функция Коллатца, которая хоть и выглядит просто, но вероятно для доказательства завершаемости придётся пользоваться фундироваными множествами). И красиво выглядит код который потом получается. И не должно занять много времени, по идее.

А функция Коллатца интересна как задачка мне, поскольку я методами решения подобных задач не пользовался (они больше для программирования, чем для доказательств). Единственное требование, ( alysnix) завершаемость функции должна быть доказана (до меня), и то что мы хотим ещё доказать про функцию тоже должно быть доказано (чтобы я там пол жизни не тратил на выдумывание доказательств, я всё таки не математик. А просто переложил существующие док-ва на кок).

Поэтому я пойду с мьютексов, с вашего позволения. Ну и это всё если времени хватит (сейчас как раз есть немного).

Мне не нравится идея, что правильный, но недоказуемый (а по Гёделю такой точно есть) код нельзя скомпилировать.

Я совсем не уверен что это верная трактовка теоремы о неполноте в данном случае. Правда я не специалист по логике. Поэтому то что сказано ниже, лишь моё представление. Если есть специалисты, пусть поправят.

Теорема о неполноте действительно утверждает что непротиворечивая система неполна. И мы надеемся что зависимые типы - непротиворечивая система. Но штука в том, что в коке можно формулировать утверждения об утверждениях (т.е. переходить на логики более «высоких» уровней). Это, на сколько я понимаю, и в математике происходит. Т.е. можно пытаться рассматривать аксиомы о системе аксиом и об утверждениях в этой (первой) системе аксиом. Ну и пытаться доказать в новой системе требуемое изначально утверждение. Правда в новой системе опять найдётся недоказуемое утверждение. Но можно опять же попробовать создать систему «уровнем выше». И так до бесконечности.

Собственно зависимые типы - это не отдельная система аксиом, а система в которой можно порождать системы высшего порядка (если я верно это формулирую). Поэтому я и сомневаюсь в верной трактовке теоремы о неполноте.

Так или иначе, я возьмусь утверждать (без доказательств), что не существует алгоритма, с которым бы встретился средний программист и который нельзя было бы реализовать на коке теоретически.

Тут правда вопрос в практике будет... но это другой вопрос..

В Typed Racket всегда можно завернуть в cast к нужному типу, если проверялка не может доказать корректность, но программист точно уверен (в коде будет добавлена динамическая проверка на случай, если программист всё-таки неправ).

На коке тоже можно поотключать все проверки. или изобразить динамический тип. Или даже сделать каст любого типа к любому.

Но кок не про «написать любой ценой чтоб тесты прошло», а скорее про «чтобы мышь не проскользнула если умения хватит».

В смысле? Оно запустит для всех k от 1 до 100000000000 при компиляции?

я думаю ты уже выяснил этот момент для себя, всё таки для ясности отвечу: нет, оно просто завершит функцию по достижению переданного числа шагов, если заворачивать в монаду.

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

Есть другие способы. Можно доказать что функция завершается и передать это доказательство Коку в аргументе определяемой функции.

Я может попробую изобразить на досуге, но я этим не занимался, вероятно займёт какое-то время.

И я ещё обещался написать про мьютексы.

Честно говоря задачка про мьютексы не выглядит интересной для меня, поскольку там точно всё получится. Я подобное писал вот здесь https://github.com/andreykl/crosses-zeros/blob/master/Lib.idr (когда читал книжку Бреди про Идрис, там прекрасные примеры). Тут надо смотреть на тип GameCmd который обеспечивает переход игры из одного состояния в другое и при попытке перейти не вовремя, будет ошибка времени компиляции. Ну собственно этот код взять и переписать чуток да и всё.

Но эта задачка выглядит интересной с точки зрения показать: там легко всё понять в самой постановке задачи (последовательность из n-мьютексов это как бы не функция Коллатца, которая хоть и выглядит просто, но вероятно для доказательства завершаемости придётся пользоваться фундироваными множествами). И красиво выглядит код который потом получается. И не должно занять много времени, по идее.

А функция Коллатца интересна как задачка мне, поскольку я методами решения подобных задач не пользовался (они больше для программирования, чем для доказательств). Единственное требование, ( alysnix) завершаемость функции должна быть доказана (до меня), и то что мы хотим ещё доказать про функцию тоже должно быть доказано (чтобы я там пол жизни не тратил на выдумывание доказательств, я всё таки не математик. А просто переложил существующие док-ва на кок).

Поэтому я пойду с мьютексов, с вашего позволения. Ну и это всё если времени хватит (сейчас как раз есть немного).

Мне не нравится идея, что правильный, но недоказуемый (а по Гёделю такой точно есть) код нельзя скомпилировать.

Я совсем не уверен что это верная трактовка теоремы о неполноте в данном случае. Правда я не специалист по логики. Поэтому то что сказано ниже, лишь моё представление. Если есть специалисты, пусть поправят.

Теорема о неполноте действительно утверждает что непротиворечивая система неполна. И мы надеемся что зависимые типы - непротиворечивая система. Но штука в том, что в коке можно формулировать утверждения об утверждениях (т.е. переходить на логики более «высоких» уровней). Это, на сколько я понимаю, и в математике происходит. Т.е. можно пытаться рассматривать аксиомы о системе аксиом и об утверждениях в этой (первой) системе аксиом. Ну и пытаться доказать в новой системе требуемое изначально утверждение. Правда в новой системе опять найдётся недоказуемое утверждение. Но можно опять же попробовать создать систему «уровнем выше». И так до бесконечности.

Собственно зависимые типы - это не отдельная система аксиом, а система в которой можно порождать системы высшего порядка (если я верно это формулирую). Поэтому я и сомневаюсь в верной трактовке теоремы о неполноте.

Так или иначе, я возьмусь утверждать (без доказательств), что не существует алгоритма, с которым бы встретился средний программист и который нельзя было бы реализовать на коке теоретически.

Тут правда вопрос в практике будет... но это другой вопрос..

В Typed Racket всегда можно завернуть в cast к нужному типу, если проверялка не может доказать корректность, но программист точно уверен (в коде будет добавлена динамическая проверка на случай, если программист всё-таки неправ).

На коке тоже можно поотключать все проверки. или изобразить динамический тип. Или даже сделать каст любого типа к любому.

Но кок не про «написать любой ценой чтоб тесты прошло», а скорее про «чтобы мышь не проскользнула если умения хватит».

В смысле? Оно запустит для всех k от 1 до 100000000000 при компиляции?

я думаю ты уже выяснил этот момент для себя, всё таки для ясности отвечу: нет, оно просто завершит функцию по достижению переданного числа шагов, если заворачивать в монаду.

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

Есть другие способы. Можно доказать что функция завершается и передать это доказательство Коку в аргументе определяемой функции.

Я может попробую изобразить на досуге, но я этим не занимался, вероятно займёт какое-то время.

И я ещё обещался написать про мьютексы.

Честно говоря задачка про мьютексы не выглядит интересной для меня, поскольку там точно всё получится. Я подобное писал вот здесь https://github.com/andreykl/crosses-zeros/blob/master/Lib.idr (когда читал книжку Бреди про Идрис, там прекрасные примеры). Тут надо смотреть на тип GameCmd который обеспечивает переход игры из одного состояния в другое и при попытке перейти не вовремя, будет ошибка времени компиляции. Ну собственно этот код взять и переписать чуток да и всё.

Но эта задачка выглядит интересной с точки зрения показать: там легко всё понять в самой постановке задачи (последовательность из n-мьютексов это как бы не функция Коллатца, которая хоть и выглядит просто, но вероятно для доказательства завершаемости придётся пользоваться фундироваными множествами). И красиво выглядит код который потом получается. И не должно занять много времени, по идее.

А функция Коллатца интересна как задачка мне, поскольку я методами решения подобных задач не пользовался (они больше для программирования, чем для доказательств). Единственное требование, alysnix завершаемость функции должна быть доказана (до меня), и то что мы хотим ещё доказать про функцию тоже должно быть доказано (чтобы я там пол жизни не тратил на выдумывание доказательств, я всё таки не математик. А просто переложил существующие док-ва на кок).

Поэтому я пойду с мьютексов, с вашего позволения. Ну и это всё если времени хватит (сейчас как раз есть немного).

Мне не нравится идея, что правильный, но недоказуемый (а по Гёделю такой точно есть) код нельзя скомпилировать.

Я совсем не уверен что это верная трактовка теоремы о неполноте в данном случае. Правда я не специалист по логики. Поэтому то что сказано ниже, лишь моё представление. Если есть специалисты, пусть поправят.

Теорема о неполноте действительно утверждает что непротиворечивая система неполна. И мы надеемся что зависимые типы - непротиворечивая система. Но штука в том, что в коке можно формулировать утверждения об утверждениях (т.е. переходить на логики более «высоких» уровней). Это, на сколько я понимаю, и в математике происходит. Т.е. можно пытаться рассматривать аксиомы о системе аксиом и об утверждениях в этой (первой) системе аксиом. Ну и пытаться доказать в новой системе требуемое изначально утверждение. Правда в новой системе опять найдётся недоказуемое утверждение. Но можно опять же попробовать создать систему «уровнем выше». И так до бесконечности.

Собственно зависимые типы - это не отдельная система аксиом, а система в которой можно порождать системы высшего порядка (если я верно это формулирую). Поэтому я и сомневаюсь в верной трактовке теоремы о неполноте.

Так или иначе, я возьмусь утверждать (без доказательств), что не существует алгоритма, с которым бы встретился средний программист и который нельзя было бы реализовать на коке теоретически.

Тут правда вопрос в практике будет... но это другой вопрос..

В Typed Racket всегда можно завернуть в cast к нужному типу, если проверялка не может доказать корректность, но программист точно уверен (в коде будет добавлена динамическая проверка на случай, если программист всё-таки неправ).

На коке тоже можно поотключать все проверки. или изобразить динамический тип. Или даже сделать каст любого типа к любому.

Но кок не про «написать любой ценой чтоб тесты прошло», а скорее про «чтобы мышь не проскользнула если умения хватит».