Здравствуйте, 1115, Вы писали:

1>>>>а может можно придумать высокоуровневый язык для описания доказательств теорем и вообще любых математических утверждений?
GZ>>>И назовем его SML!!!! (или кто-то уже делал такой?)

Т>>SML — не для "описания доказательств теорем", а для "программироваия систем доказательств".
1>Собственно HOL и Coq , ровно также как и LCF (ради которого был создан ML) ---- написаны на ML.
1>не думаю что это будет верх эволюции.

А что, собственно, ты называешь "высокоуровневый язык"?
Например, C++ это высокоуровневый язык? Или это такой же ассемблер как HOL. Собственно в чем разница между C++ и ассеблером. Разница в том, что к C++ прилагается компилятор, который кострукции языка умеет отображать в ассемблер. Тогда, по аналогии, HOL — не ассемблер (ассемлер в чистом виде это определение доказательства, как последовательности из формул, в которой каждая следующая получается применением правил вывода к предыдущим). И хотя идеологически HOL внутри это именно это определение и есть, то для пользователя, HOL идет вместе со свякими политиками применения правил вывода т.е. средством отобраения твоих "высокоуровневых идей" в "доказательство по определению". Так же к HOL прилагается ML, на котором ты можешь написать свои собственные патерны, и способы "отображения идей". И получается, что HOL, идет вместе с тем, что программисты называют мета-программированием.

Или под "высокоуровневым языком" ты понимаешь что-нить типа managed? Т.е. язык который, кроме отображения в ассемблер предлагает, что-то новое, не существующее на уровне процессорных команд. Я тут говорю о, например, сборке мусора и механизма эксепшенов. Если так то возникает вопрос "Нафига оно надо или как это привязать к определению?". Дело тут в том, что в программировании цель — решение задачи пользователя, а комп, процессорный код, интерпретатор, ... это всего лишь средства достижения этой цели. По-этому пользователю не важно произвел ли ты код для процессора его компа или будет работать интерпретатор, ему важно решает ли результат твоей работы его проблему. С доказательствами все не так, а наоборот. Ценность не в ответе да/нет (эта теорема верна/неверна), а именно в этой самой цепочке формул, которая доказывает ответ да/нет. Т.е. по програмерской аналогии, ценность имеет только ассемблерный код, и соотвественно ценность имеет только компилируемый язык.