Отправляет email-рассылки с помощью сервиса Sendsay

Искусственный интеллект

Рассылка закрыта

При закрытии подписчики были переданы в рассылку "Раскрутка сайта для начинающих" на которую и рекомендуем вам подписаться.

Вы можете найти рассылки сходной тематики в Каталоге рассылок.

←   Октябрь 2005   →
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
Автор
gvozdok

Статистика

4 подписчиков
0 за неделю
←   Все выпуски   →

Искусственный интеллект


Информационный Канал Subscribe.Ru

Искусственный интеллект | Обсуждение статей | Написать письмо

Обсудить эту статью >>

Система Coq (Кок)

Здравствуйте, уважаемые читатели!

Во-первых, позвольте сделать объявление. Если вы регистрировались на нашем форуме в промежутке примерно с 4 по 14 октября, то из-за ошибки в настройках сервера вы могли не получить подтверждающего письма. В связи с этим приношу свои извинения и прошу тех, кто попал в промежуток, перегистрироваться заново.

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

Несколько лет назад на одном из форумов я наткнулся на не вполне адекватное замечание, что я - плохой программист, так как пользуюсь отладчиками. Оказалось, автор претензии выступает за какой-то новомодный язык под названием Caml и при работе на котором, якобы, отладчики не нужны. Тогда мы с этим человеком просто поругались, а позднее, на совершенно другом форуме, я спросил уже у более адекватного собеседника, действительно ли в языке Caml не нужны отладчики?

Он ответил, что это, конечно, слишком сильное утверждение, но в языке действительно есть мощный механизм разворачивания кодовых конструкций, чем-то напоминающий шаблоны в Си++, который позволяет в каких-то случаях создавать сложные программы и гарантировано без логических ошибок.

Кстати, можно поразмыслить о роли шаблонов в Си++. Ведь в более позднем языке, Java, их нет. С другой стороны, они достаточно красивы. Куда же они делись?

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

Это сделано для того, чтобы одни и теже процедуры можно было бы использовать для разных типов, причём эффективно. В Java то же достигается путём тотального применения идеологии ООП: если класс или функция должны работать для нескольких типов, то они должны быть реализованы для базового виртуального (абстрактного) класса, а эти несколько типов должны быть его наследниками. Это действительно логичнее и это становится очевидно, когда пытаешься написать шаблон в предположении, что класс-аргумент имеет какие-то методы или члены: выясняется, что механизма объявления этого факта не существует.

То есть, Java, вроде бы, логичнее. С другой стороны, почему мы считаем объекты и классы разными сущностями и не позволяем передавать в функцию вторые?

Ну ладно, вернёмся к Caml.

Насколько я понял, это так называемый функциональный язык программирования. Функциональный - это означает, что у его функций исключены так называемые побочные эффекты. Это значит, что если в любом выражении встречается вызов функции, то это выражение в точности эквивалентно выражению, в котором вызов функции заменён на возвращённое ей значение. Как в математике.

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

Разумеется, те, кто хорошо знаком с программированием, знают, что ограничения - это далеко не всегда плохо. Например, во многих современных языках использовать можно только те переменные, которые объявлены. Это ограничение, но оно приносит пользу, так как позволяет избегать ошибок. Без этого ограничения малейшая опечатка в имени переменной оставалась бы незамеченной компиллятором.

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

Ну вот. Я обнаружил в интернете несколько баталий давностью 2-3 года, состоявшихся между сторонниками Caml и сторонниками "императивного" (обычного) программирования. Уровень дискуссий, разумеется, не намного отличался от уровня той ругани, в которой участвовал я сам несколько лет назад.

В общем, фактически, ничего понять из дискуссий оказалось нельзя.

Ещё тогда, много лет назад, я узнал об ещё одном факте. Оказывается, на языке Caml (OCaml) благодаря его супер-пупер возможностям, написана одна система, относящаяся к категории proff assistant (помощник в доказательстве). Эта система, якобы, позволяет ввести в неё любое доказательство математической теоремы (например, теоремы Пифагора) и проверить, правильное оно или нет. Кроме того, под руководством человека, система способна теоремы даже доказывать. То есть, как мне представилось, это своеобразный "логический Excel".

Система называется Coq и разработана каким-то французским компьютерным институтом, который занимается, в том числе, и искусственным интеллектом.

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

Теперь я попытаюсь публично в этом всём разобраться, а начну с ситемы Coq. Coq по-французски значит петух.

Ну вот.

Официальный сайт системы находится по адресу http://coq.inria.fr/

Скачать (по ФТП) её можно отсюда (для Виндов): ftp://ftp.inria.fr/INRIA/coq/V8.0/Coq-8.0-Win.zip

Документация на английском находится тут: http://coq.inria.fr/doc-eng.html

Ниже я представляю на ваш суд мой перевод tutorial, пока я перевёл только несколько первых разделов. Пардон, я набрал его с форматированием в Word, а как наиболее чисто перенести в HTML без внешних стилей для DreamWeaver и рассылки - не знаю.

***

Словарик

Английский

Русский

coq

кок

tutorial

пособие

Logical Framework

Раздел логики

Calculus of Inductive Constructions

исчисление индуктивных конструкций

specification (объектное существительное)

класс

specification (глагольное существительное)

классификация

declaration

объявление

formal axiomatisation

система формальных аксиом

specification language

язык классификаций

(system) sort

(системный) разряд

proposition

суждение

set

набор

bound variable

связанная переменная

 

Система автоматизированного доказывания Кок (Coq)

Пособие

Кок (Coq) – это система автоматизированного доказывания, построенная на основе такого раздела логики, как исчисление индуктивных конструкций. С помощью неё можно вживую строить формальные доказательства, а также работать с функциональными программами без разрыва с их описательной частью. Система работает в виде компьютерной программы на множестве платформ и обращаться к ней можно через ряд пользовательских интерфейсов. Данный документ не ставит целью охватить перечень всех возможностей Кока, а представляет собой пособие по основным возможностям языка классификаций, который называется Галина и на котором можно разрабатывать системы формальных аксиом, а также по основным инструментам доказывания. За более подробными сведениями следует обращаться в справочное руководство по Коку, а также к новой книге…

Мы предполагаем, что потенциальный пользователь установил Кок на своём компьютере, что он вызвал Кок в стандартном «телетайпном» окне командной строки и что он не применяет никакого специализированного интерфейса. …

Основы исчисления предикатов

Обзор языка классификаций Галина

Разработка формализма в Галине состоит из последовательности описаний и определений. Кроме того, Коку можно также отдавать команды, которые не входят в разработку формализма, а являются запросами информации или вызовами служебных функций. Например, команда

Coq < Quit.

перевод на русский: Quit – выйти.

заканчивает текущий сеанс работы.

Описания

Описание именует классификацию, связывает имя с классом.

Имя, грубо говоря, соответствует идентификатору в языках программирования, то есть, строчке из букв, цифр и некоторых других символов ASCII наподобие символа подчёркивания (_) и одинарной кавычки, начинающейся с буквы. В Галине используется чувствительность к регистру, так что имена A и a отличаются друг от друга. Некоторые строчки зарезервированы как ключевые слова Кока и поэтому их нельзя использовать в качестве пользовательских идентификаторов.

Класс – это формальное выражение, которое классифицирует некое (объявляемое) понятие. Имеется три основных класса: логических суждений, математических наборов и абстрактных типов. Это три системных разряда, которые называются соответственно Prop, Set и Type, которые сами по себе относятся к разряду неделимых абстрактных типов.

Перевод на русский: Proposition – суждение, Set – набор, Type – тип.

Каждое правильное выражение e в языке Галина связано с классом, который, в свою очередь, является правильным выражением и называется типом t(E) первого выражения. Утверждение, что e относится к типу E мы записываем в виде e:t(E). Вы можете попросить Кок сообщить Вам тип правильного выражения при помощи команды Check:

Coq < Check O.
0
     : nat

Перевод на русский: Check – проверь, natural – натуральное.

Теперь мы знаем, что идентификатор O (имя ‘O’ не следует путать с цифрой ‘0’, которая не является правильным идентификатором!) известен в текущем контексте, а его типом является класс nat. Этот класс сам по себе классифицируется как математический набор, что мы можем быстро проверить:

Coq < Check nat.
nat
     : Set

Перевод на русский: Check – проверь, natural – натуральное, Set – набор.

Класс Set сам относится к абстрактным типам, и является одним из основных разрядов языка Галина, а понятия nat и O – это вторичные понятия, которые определяются в начальном арифметическом сценарии, который автоматически исполняется при запуске Кока.

Начнём с заведения так называемого имени раздела. Роль разделов заключается в организации процесса моделирования, ограничивая область видимости параметров, предположений и определений. Кроме того, они предоставляют удобный способ переделать заново часть разработки.

Coq < Section Declaration.

Перевод на русский: Section – раздел, Declaration – объявление.

Используя имеющиеся у нас знания, мы теперь можем ввести в систему объявление, соответствующее фразе неформальной математики «пусть n является натуральным числом».

Coq < Variable n : nat.
n is assumed

Перевод на русский: Variable – переменная, natural – натуральное, is assumed – допущено.

Если мы хотим записать более подробное утверждение, например «пусть n является положительным натуральным числом», то придётся добавить ещё одно объявление, которое объявит явное предположение Pos_n и классифицирует его при помощи логического суждения:

Coq < Hypothesis Pos_n : (gt n 0).
Pos_n is assumed

Перевод на русский: Hypothesis – предположение, Positive – положительный,  (гипотеза), greaterthan – больше чем

В самом деле, мы можем проверить, что отношение gt известно в текущем контексте и имеет нужный тип:

Coq < Check gt.
gt
     : nat -> nat -> Prop

Перевод на русский: Check – проверь, greaterthan – больше чем, natural – натуральное, Proposition – суждение.

это нам скажет, что gt есть функция, берущая два аргумента типа nat и дающая в результате логическое суждение. Здесь используется тот же подход, что и в функциональном программировании: мы можем соединить (классифицирующий) тип nat с (абстрактным) типом логических суждений Prop с помощью стрелки (конструктора функций) и получить в результате функциональный тип nat->Prop:

Coq < Check (nat -> Prop).
nat -> Prop
     : Type

Перевод на русский: Check – проверь, natural – натуральное, Proposition – суждение, Type – тип.

который можно дальше соединить снова с nat и получить тип nat->nat->Prop двоичных отношений между натуральными числами. Фактически, nat->nat->Prop есть сокращение для nat->(nat->Prop).

Понятие действия функции составляется обычным способом. Выражение f типа A->B может подействовать на выражение e типа A и тогда получится выражение (f e) типа B. Здесь становится понятно, что выражение (gt n) построено правильно и имеет тип nat->Prop и что, таким образом, выражение (gt n O), которое есть сокращение выражения ((gt n) O), является правильно построенным суждением.

Coq < Check gt n O.
n > 0
     : Prop

Перевод на русский: Check – проверь, graterthan – больше чем, Proposition – суждение.

Определения

Начальный сценарий содержит несколько арифметических определений: nat определен как математический набор (тип Set), постоянные O, S, plus определены как объекты типов nat, nat->nat и nat->nat->nat соответственно. Вы можете вводить новые определения, каждое из которых должно связывать имя с правильно построенным значением. Например, Вы можете ввести постоянную odin, определив её как число, следующее за нулём:

Coq < Definition odin := (S O).
odin is defined

Перевод на русский: Definition – определение, is defined - определено.

Можно (но необязательно) указать требуемый тип:

Coq < Definition dva : nat := S odin.
dva is defined

Перевод на русский: Definition – определение, natural – натуральное, is defined – определено.

Вот как можно определить удваивающую функцию dvajdy, которая берёт один аргумент m типа nat и даёт в результате (plus m m):

Coq < Definition dvajdy (m:nat) := plus m m.
dvajdy is defined

Перевод на русский: Definition – определение, plus – плюс, is defined - определено.

Это определение вводит новую постоянную dvajdy, которая определяется как выражение fun m:nat => plus m m. Смысл понятия fun можно объяснить следующим образом. Выражение fun x:A => e является в данном контексте правильно построенным выражением типа A->B, если выражение e стало бы правильно построенным выражением типа B при добавлении в данный контекст объявления, что x принадлежит к типу A. Здесь получается, что x – это связанная или «вспомогательная» переменная в выражении fun x:A => e. Мы могли бы определить dvajdy как fun n:nat => (plus n n).

Связанные (локальные) переменные и свободные (глобальные) переменные можно смешивать. Например, можно определить функцию, которая добавляет к своему аргументу постоянную n вот так:

Coq < Definition dobav_n (m:nat) := plus m n.
dobav_n is defined

Перевод на русский: Definition – определение, natural – натуральное, plus – плюс, is defined – определено.

Обратите внимание, что в этом определении нельзя заменить формальный параметр (связанную переменную) с m на n не перекрыв свободного значения n и не нарушив смысла определяемого понятия.

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

Переменная становится связанной, когда о ней что-то сказано во вне, и тогда для смысла выражения уже не имеет значения, какой буквой переменная обозначена. Связывание переменных широко известно в логике, где оно происходит при квантификации. Мы можем квантифицировать суждение, например, m>0, квантором всеобщности и получить всеобщее суждение "m m>0. Эта операция доступна в Коке при помощи выражения forall m:nat, gt m O. Так же, как и в случае связывания при определении функции, мы обязаны явно объявить тип квантифицированной переменной.

Проверяем:

Coq < Check (forall m:nat, gt m 0).
forall m : nat, m > 0
     : Prop

Перевод на русский: Check – проверь, forall – длявсех, greaterthan - большечем, natural – натуральное, Proposition – суждение.

Мы можем начать с чистого листа, очистив содержимое текущего раздела:

Coq < Reset Declaration.

Перевод на русский: Reset – переустанови, Declaration – объявление.

***

Обсудить эту статью >>

Subscribe.Ru
Поддержка подписчиков
Другие рассылки этой тематики
Другие рассылки этого автора 		Подписан адрес:
Код этой рассылки: comp.soft.db.artificial
Архив рассылки 		Отписаться
Вспомнить пароль
В избранное