tchingizавтор
Разумеется, поскольку чистое лямбда-исчисление полно по Тьюрингу, мы не можем даже надеять-
ся, что нам удастся провести точный анализ типов для всех примитивов. Например, нет никакого
надежного способа понять, возвращает ли программа
if <долгое и сложное вычисление> then true else (\lambda x.x)
булевское значение или функцию, не запустив сначала это долгое и сложное вычисление и не посмотрев,
выдало ли оно истинное или ложное значение. В общем случае, долгое и сложное вычисление может
вообще не завершиться, и тогда всякий вычислитель, который попытается точно предсказать его исход,
тоже никогда не выдаст результата.


связка "разумеется, по скольку полно по Тьюрингу ... не можем даже надеяться" действительно очевидна?
А то мне чтото не очень ))

так и простое зацикливание формально нераспознаваемо (в общем случае!)
а не то, что "долгое и сложное", которое вообще-то завершаемое и коррекное, но в нереальное космическое время

А как в книжке этот вопрос увязывают с типами?

tchingizхотят узнать тип оператора if.


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

Блин, мне, когда студентом был, дискретную математику вещал профессор Горбатов В. А.
(ввел в дискретную математику понятие мографа, продвинул многосортную логику).
Его книжки-учебники (есть в е-библиотеках) можно почитать (Например, Горбатов В.А. — Фундаментальные основы дискретной математики. Информационная математика. и пр.). То есть учебников много, но он отличается типаконкретностью.

P.S. А я тоже до того, как стал забабло-кодером БД, нетленки с ангельского переводил как основная деятельность на работе.

tchingizно почему "мы не можем даже надеять-
ся, что нам удастся провести точный анализ типов для всех примитивов."
не понятно все равно.

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

tchingiz
Пилотажный, ты кому халло говоришь?
Тому, кто тоже нетленки с ангельского переводит на работе?


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

переводчик - второй автор, когда текст очень специализированный или, так сказать, высокохудожественный

Исходно - машина Тьюринга, тезис Черча, нормальный алгоритм Маркова, лямбда-исчисление, ... - это формальные определения алгоритма. Есть формальный алгоритм = возможна программа.
Вопрос философский - "Что возможно запрограммировать и что невозможно?".
Например, частично рекурсивные функции: формальный алгоритм (формальную программу) возможно представлять как обобщенную функцию - вход-аргумент-ввод и выход-значения-вывод. Вопрос "Всякую ли функцию возможно запрограммировать?". Ответ - те, которые возможно выразить-представить через частично рекурсивные функции. Ответ - и те, которые выразимы через машину Тьюринга. ...

Ну и язык программирования 'полон по Тьюрингу' = любой формальный алгоритм возможно записать на нем.

И обычно теория отрывается от практики, а практика обычно бывает шире и не описывается теорией.