Правильная работа программ

[arseniiv]

realeugene в сообщении #1383400 писал(а):

С противопоставлением моделей вычислений.

А. Ну там ситуацию особо не развернёшь дальше уже написанного. Те люди, видимо, хотели, чтобы можно было делать вычисления например со строками над произвольным алфавитом, при этом не кодируя их натуральными числами. И думали, что в частности машины Минского могут быть определены только для последних. Изначально, видимо, действительно большинство регистровых машин определялись специально для натуральных чисел, но ничто не мешает иному, особенно когда машина не поминает каких-то непримитивных свойств типа делимости. В общем само по себе внимания не стоит, это было просто дополнение для тех, кому могло быть скучно.

realeugene в сообщении #1383400 писал(а):

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

Возможно… Если говорить только о том направлении, что задал ТС, с соответствующим уровнем, наверно не нужно. В общем случае — сейчас не имею понятия.

[_Ivana]

george66 в сообщении #1383267 писал(а):

Если не вникать глубоко, принцип математической индукции работает

Если не вникать глубоко, то некто Денис Москвин в своих курсах по Хаскелю на Степике будет давать задание на доказательство того, что тип данных список является функтором. И ожидать доказательство по индукции. Но если Пирсу в ТАПЛе это простительно, у него там аппликативная модель вычислений, то в Хаскеле тем же методом доказывается, что все списки имеют конечную длину Мой короткий стримчик про это (старательно избегал слов типа "функтор" и подобных, чтобы не пугать неподготовленную аудиторию)

Но степень желаемой глубины вникания каждый определяет для себя сам, да.

[realeugene]

_Ivana в сообщении #1383468 писал(а):

то в Хаскеле тем же методом доказывается, что все списки имеют конечную длину

Не совсем. Не очень знаком с Хаскелем, но мне кажется, что вы в своём видео доказали по индукции, что все списки в Хаскеле, которые имеют длину, имеют конечную длину. Или в Хаскеле не бывает частичных функций?

[arseniiv]

Бывают, конечно. В любом тьюринг-полном языке бывают, а если (негуманно) потребовать вместе с функцией доказывать её тотальность, тьюринг-полнота пропадёт.