2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2
 
 Re: Правильная работа программ
Сообщение21.03.2019, 22:59 
Заслуженный участник


27/04/09
28128
realeugene в сообщении #1383400 писал(а):
С противопоставлением моделей вычислений.
А. Ну там ситуацию особо не развернёшь дальше уже написанного. Те люди, видимо, хотели, чтобы можно было делать вычисления например со строками над произвольным алфавитом, при этом не кодируя их натуральными числами. И думали, что в частности машины Минского могут быть определены только для последних. Изначально, видимо, действительно большинство регистровых машин определялись специально для натуральных чисел, но ничто не мешает иному, особенно когда машина не поминает каких-то непримитивных свойств типа делимости. В общем само по себе внимания не стоит, это было просто дополнение для тех, кому могло быть скучно.

realeugene в сообщении #1383400 писал(а):
Математика, в которой совершенно излишне углубляться в нестандартные модели арифметики и ограничивать себя логикой первого порядка.
Возможно… Если говорить только о том направлении, что задал ТС, с соответствующим уровнем, наверно не нужно. В общем случае — сейчас не имею понятия.

 Профиль  
                  
 
 Re: Правильная работа программ
Сообщение22.03.2019, 11:56 


05/09/12
2587
george66 в сообщении #1383267 писал(а):
Если не вникать глубоко, принцип математической индукции работает

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

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

 Профиль  
                  
 
 Re: Правильная работа программ
Сообщение22.03.2019, 16:11 


27/08/16
9426
_Ivana в сообщении #1383468 писал(а):
то в Хаскеле тем же методом доказывается, что все списки имеют конечную длину
Не совсем. Не очень знаком с Хаскелем, но мне кажется, что вы в своём видео доказали по индукции, что все списки в Хаскеле, которые имеют длину, имеют конечную длину. Или в Хаскеле не бывает частичных функций?

 Профиль  
                  
 
 Re: Правильная работа программ
Сообщение22.03.2019, 19:14 
Заслуженный участник


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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 19 ]  На страницу Пред.  1, 2

Модераторы: Karan, Toucan, PAV, maxal, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group