Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Эта статья о языке программирования Curry (названном в честь математика и логика). Для математиков и логиков см. Haskell Curry . Для техники информатики см. Каррирование .
Карри
Парадигмафункциональная , логическая , нестрогая, модульная
РазработаноМайкл Ханус, Серджио Антой и др.
Печатная дисциплинастатичный , сильный , предполагаемый
Операционные системыпортативный
Интернет сайтКарри
Основные реализации
PAKCS (с Prolog в качестве цели), mcc (с C в качестве цели), KiCS2 (с Haskell в качестве цели)
Под влиянием
Haskell и Prolog

Curry [1] - экспериментальный язык программирования функциональной логики [2], основанный на языке Haskell . Он объединяет элементы функционального и логического программирования, включая интеграцию программирования в ограничениях .

Это почти надмножество Haskell, в котором отсутствует поддержка в основном для перегрузки с использованием классов типов , которые некоторые реализации в любом случае предоставляют в качестве расширения языка, например Münster Curry Compiler. [3]

Основы функционально-логического программирования [ править ]

Основные понятия [ править ]

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

двойной х = х + х

Выражение « двойная 1 » заменяется на 1 + 1 . Последнее можно заменить на 2, если мы интерпретируем оператор « + » как определяемый бесконечным набором уравнений, например, 1 + 1 = 2 , 1 + 2 = 3 и т. Д. Аналогичным образом можно оценить вложенные выражения (где заменяемые подвыражения заключены в кавычки):

'двойной (1 + 2)' → '(1 + 2)' + (1 + 2) → 3 + '(1 + 2)' → '3 + 3' → 6

Также существует другой порядок вычисления, если мы заменим аргументы операторов справа налево:

'двойной (1 + 2)' → (1 + 2) + '(1 + 2)' → '(1 + 2)' + 3 → '3 + 3' → 6

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

Как и многие функциональные языки, такие как Haskell , Curry поддерживает определение алгебраических типов данных путем перечисления их конструкторов. Например, тип логических значений состоит из конструкторов True и False , которые объявлены следующим образом:

 data  Bool  =  True  |  Ложь

Функции на логических значениях могут быть определены путем сопоставления с образцом, т. Е. Путем предоставления нескольких уравнений для разных значений аргументов:

 not  True  =  Ложь  не  Ложь  =  Верно

Принцип замены равных на равные по-прежнему действует при условии, что фактические аргументы имеют требуемую форму, например: 

not '(not False)' → 'not True' → False

Более сложные структуры данных можно получить с помощью рекурсивных типов данных . Например, список элементов, где тип элементов является произвольным (обозначается переменной типа a ), представляет собой либо пустой список « [] », либо непустой список « x: xs », состоящий из первого элемента x и список хз : 

  Список  данных a  =  []  |  : Список

Тип « Список a » обычно записывается как [a], а конечные списки x1 : x2 : ... : xn : [] записываются как [ x1 , x2 , ... , xn ] . Мы можем определять операции с рекурсивными типами с помощью индуктивных определений, в которых сопоставление с образцом поддерживает удобное разделение различных случаев. Например, операция конкатенации « ++ » в полиморфных списках может быть определена следующим образом (необязательное объявление типа в первой строке указывает, что « ++”Принимает два списка в качестве входных и создает выходной список, в котором все элементы списка имеют один и тот же неуказанный тип):

 ( ++ )  ::  [ a ]  ->  [ a ]  ->  [ a ]  []  ++  ys  =  ys  ( x : xs )  ++  ys  =  x  :  xs ++ ys

Помимо применения для различных задач программирования, операция « ++ » также полезна для определения поведения других функций в списках. Например, поведение функции last, которая возвращает последний элемент списка, может быть определено следующим образом: для всех списков xs и элементов e last xs = e, если ∃ys : ys ++ [ e ] = xs.

На основе этой спецификации можно определить функцию, которая удовлетворяет этой спецификации, используя возможности логического программирования. Подобно языкам логики, языки функциональной логики обеспечивают поиск решений для экзистенциально количественно определенных переменных. В отличие от языков чистой логики, они поддерживают решение уравнений по вложенным функциональным выражениям, так что уравнение типа ys ++ [ e ] = [1,2,3] решается путем создания экземпляра ys в списке [1,2] и e в значение 3 . В Curry можно определить последнюю операцию следующим образом:

 последний  хз  |  ys ++ [ e ]  =: =  xs  =  e  где  ys , e  бесплатно

Здесь символ « =: = » используется для эквациональных ограничений, чтобы обеспечить синтаксическое отличие от определяющих уравнений. Точно так же дополнительные переменные (т. Е. Переменные, не встречающиеся в левой части определяющего уравнения) явно объявляются как « where ... free », чтобы предоставить некоторые возможности для обнаружения ошибок, вызванных опечатками. Условное уравнение вида l | c =r применимо для редукции, если его условие c было решено. В отличие от чисто функциональных языков, где условия оцениваются только до логического значения, языки функциональной логики поддерживают решение условий путем угадывания значений неизвестных в условии. Сужение, как описано в следующем разделе, используется для решения такого рода условий.

Сужение [ править ]

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

Сужение полезно, потому что оно позволяет рассматривать функцию как отношение: ее значение может быть вычислено «в обоих направлениях». Примеры Карри из предыдущего раздела иллюстрируют это.

Как отмечалось в предыдущем разделе, сужение можно рассматривать как сокращение на графе терминов программы, и часто существует множество различных способов ( стратегий ) для сокращения данного графа терминов. Antoy et al. [4] доказали в 1990-х годах, что конкретная стратегия сужения, необходимая для сужения , является оптимальной в смысле выполнения ряда редукций для перехода к «нормальной форме», соответствующей решению, которое является минимальным среди разумных и полных стратегий. Необходимое сужение соответствует ленивой стратегии, в отличие от стратегии разрешения SLD в Prolog .

Функциональные шаблоны [ править ]

Последнее определение правила, показанное выше, выражает тот факт, что фактический аргумент должен соответствовать результату сужения выражения ys ++ [e] . Карри может выразить это свойство еще более кратко:

 last  ( ys ++ [ e ])  =  e

Haskell не допускает такого объявления, поскольку образец в левой части содержит определенную функцию ( ++ ). Такой узор еще называют функциональным . [5] Функциональные шаблоны становятся возможными благодаря объединенным функциональным и логическим возможностям Curry и поддерживают краткие определения задач, требующих глубокого сопоставления с образцом в иерархических структурах данных.

Недетерминизм [ править ]

Поскольку Curry может решать уравнения, содержащие вызовы функций с неизвестными значениями, механизм его выполнения основан на недетерминированных вычислениях, как и в логическом программировании. Этот механизм поддерживает также определение недетерминированных операций , т. Е. Операций, которые доставляют более одного результата для данного ввода. Архетип недетерминированных операций - это предопределенная инфиксная операция ? , называемый оператором выбора , который возвращает один из своих аргументов. Этот оператор определяется следующими правилами:

Икс ? у = х Икс ? у = у

Таким образом, оценка выражения 0? 1 возвращает 0, а также 1 . Вычисления с недетерминированными операциями и вычисления со свободными переменными путем сужения имеют одинаковую выразительную силу. [6]

Правила, определяющие ? показать важную особенность Карри: все правила пробуются для того, чтобы оценить некоторую операцию. Следовательно, можно определить как

 вставить  x  ys  =  x  :  ys  вставить  x  ( y : ys )  =  y  :  вставить  x  ys

операция для вставки элемента в список в неопределенной позиции, так что операция perm определена

 perm  []  =  []  perm  ( x : xs )  =  вставить  x  ( разрешить  xs )

возвращает любую перестановку данного входного списка.

Стратегии [ править ]

Из-за отсутствия побочных эффектов программа функциональной логики может выполняться с разными стратегиями. Для оценки выражений Карри использует вариант необходимой стратегии сужения , который сочетает в себе ленивое вычисление с недетерминированными стратегиями поиска. В отличие от Prolog, в котором для поиска решений используется отслеживание с возвратом, Curry не исправляет конкретную стратегию поиска. Следовательно, существуют реализации Curry, такие как KiCS2 , где пользователь может легко выбрать стратегию поиска, такую ​​как поиск в глубину (обратный поиск ), поиск в ширину , итеративное углубление или параллельный поиск.

Ссылки [ править ]

  1. ^ Майкл Ханус (ред.). «Карри: действительно интегрированный функциональный логический язык» .CS1 maint: дополнительный текст: список авторов ( ссылка )
  2. ^ Серхио Антой и Майкл Ханус (2010). «Функционально-логическое программирование». Коммуникации ACM . ACM. 53 (4): 74–85. DOI : 10.1145 / 1721654.1721675 . S2CID 14578759 . 
  3. ^ Компилятор Münster Curry
  4. ^ Серхио Антой, Рашид Эшахед и Майкл Ханус (2007). «Необходимая стратегия сужения». Журнал ACM . ACM. 47 (4): 776–822. DOI : 10.1145 / 347476.347484 . ISSN 0004-5411 . S2CID 47275506 .  
  5. ^ Antoy Sergio, Hanus Майкл (2006). «Декларативное программирование с использованием шаблонов функций». Конспект лекций по информатике . 3901 : 6–22. DOI : 10.1007 / 11680093_2 . ISBN 978-3-540-32654-0.
  6. ^ Antoy Sergio, Hanus Майкл (2006). «Перекрывающиеся правила и логические переменные в программах функциональной логики». Конспект лекций по информатике . 4079 : 87–101. DOI : 10.1007 / 11799573_9 . ISBN 978-3-540-36635-5.

Внешние ссылки [ править ]

  • Карри - Домашняя страница Карри
  • Smap - веб-среда выполнения для Curry и Haskell с различными примерами программ.
  • MCC - компилятор Münster Curry, использующий C в качестве целевого
  • PAKCS Основная реализация Curry с WWW-интерфейсом, использующая Prolog в качестве цели.
  • KiCS2 Реализация Curry, использующая Haskell в качестве цели.
  • Список рассылки Карри
  • Домашняя страница Майкла Хануса
  • Чисто функциональное ленивое недетерминированное программирование (Fischer, Kiselyov, Shan, 2009), преобразование функциональных логических программ в монадические функциональные программы (Braßel, Fischer, Hanus, Reck, 2010) по моделированию ленивого недетерминированного (логического) программирования (как в Curry ) на чисто функциональном языке ( Haskell ); такой подход может дать программисту большую гибкость в управлении стратегиями, которые - в случае Карри - встроены.