Карри (язык программирования)

Эта статья о языке программирования Curry (названном в честь математика и логика). Информацию о математике и логике см. в Haskell Curry . Чтобы узнать о технике информатики, см. Карринг .

Карри

Парадигма	функциональный , логический , нестрогий, модульный
Разработано	Майкл Ханус, Серджио Антой и др.
Разработчик	Как университет Мюнхенский университет Людвига-Максимилиана Университет Мюнстера Портлендский государственный университет Мадридский университет Комплутенсе Технический университет Мадрида
Впервые появился	1995 год ( 1995 )
Стабильная версия	3.6.0   / (10 ноября 2023 г.)
Дисциплина набора текста	статический , сильный , предполагаемый
Платформа	х86-64
ТЫ	Кроссплатформенность : Linux
Лицензия	BSD 3-пункт
Веб-сайт	карри .страницы .ps .Информатика .uni-подобный .из /карри-ланг .org
Основные реализации
PAKCS ( цель Prolog ), mcc ( C цель ), KiCS2 ( цель Haskell )
Под влиянием
Хаскель , Пролог

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

Это почти расширенный набор Haskell, но он не поддерживает все языковые расширения Haskell. В отличие от Haskell, Curry имеет встроенную поддержку недетерминированных вычислений, включающих поиск.

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

Основные понятия

Функциональная программа — это набор функций, определяемых уравнениями или правилами. Функциональное вычисление состоит из замены подвыражений равными (относительно определений функций) подвыражениями до тех пор, пока замены (или сокращения) не станут невозможны и не будет получено значение или нормальная форма. Например, рассмотрим функцию 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 поддерживает определение алгебраических типов данных путем перечисления их конструкторов. Например, тип логических значений состоит из конструкторов Правда и False , которые объявляются следующим образом:

 данные   Bool   =   Истина   |    ЛОЖЬ 

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

 не   правда   =   ложь 
  не   ложь   =   правда 

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

не '(не ложь)' → 'не правда' → ложь
 

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

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

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

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

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

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

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

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

Сужение

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

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

Как отмечалось в предыдущем разделе, сужение можно рассматривать как сокращение графа терминов программы, и часто существует множество различных способов ( стратегий ) сокращения данного графа терминов. Антой и др. В 1990-х годах было доказано, что конкретная стратегия сужения ( need сужение ) оптимальна в смысле выполнения ряда сокращений для достижения «нормальной формы», соответствующей решению, которое является минимальным среди надежных и полных стратегий. Необходимое сужение соответствует ленивой стратегии, в отличие от SLD-разрешения стратегии Пролога .

Функциональные шаблоны

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

 последний   (  ys  ++  [  e  ])   =   e 

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

Недетерминизм

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

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

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

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

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

операция вставки элемента в список в неопределенную позицию, чтобы операция Пермь определяется

 перм   []       =   [] 
  перм   (  x  :  xs  )   =   вставить   x   (  перм   xs  ) 

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

Стратегии

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

Внешние ссылки

• Официальный веб-сайт
• Smap — веб-среда выполнения для Curry и Haskell с различными примерами программ.
• Пакеты Curry — коллекция программных пакетов для Curry.
• MCC — компилятор Münster Curry, ориентирован на C
• PAKCS Основная реализация Curry, ориентированная на Пролог.
• KiCS2 Реализация Curry, ориентированная на Haskell.
• Curry2Go Реализация Curry, ориентированная на Go и поддерживающая честный параллельный поиск.
• Список рассылки Карри
• Домашняя страница Михаэля Хануса
• Чисто функциональное ленивое недетерминированное программирование (Фишер, Киселев, Шан, 2009), Преобразование программ функциональной логики в монадические функциональные программы (Брассель, Фишер, Ханус, Рек, 2010) по моделированию ленивого недетерминированного (логического) программирования (например, в Карри) ) на чисто функциональном языке ( Haskell ); такой подход может дать программисту больше гибкости в контроле над стратегиями, которые — в случае Карри — являются встроенными.