Определить понятие пар, используя логику высшего порядка

Пересматриваю курс по автоматизированному мышлению и не совсем понимаю, как ответить на этот вопрос:

Покажите, как можно определить понятие пар (x, y) в логике высшего порядка с использованием лямбда-абстракции. Определите функцию π1, которая возвращает первый элемент такой пары. Наконец, покажите, что π1(x, y) = x.

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


logic functional-programming church-encoding lambda-calculus
person Cole Zimmerman    schedule 19.05.2017    source источник
comment
Вот исполняемый код для вашего любимого браузера (для простоты я использую тип Number): const Pair = (x, y) => f => f(x, y); const fst = pair => pair((x, y) => x); fst(Pair(2, 3)) === 2; дает true   -  person    schedule 19.05.2017

Ответы (3)


arrow_upward
3
arrow_downward

Ну вот

PAIR := λx. λy. λp. p x y

π1 := λp. p (λx. λy. x)

π2 := λp. p (λx. λy. y)

π1 (PAIR a b) => a

π2 (PAIR a b) => b

Проверьте вики-запись на церковное кодирование, где также есть несколько хороших примеров.

person Mulan    schedule 19.05.2017

arrow_upward
2
arrow_downward

Основная тема этого вопроса — понять, как данные могут быть представлены в виде функций. Когда вы работаете с другими парадигмами, нормальный способ мышления таков: «данные = что-то, что хранится в переменной» (может быть массив, объект, любая структура, которую вы хотите).

Но когда мы занимаемся функциональным программированием, мы также можем представлять данные в виде функций. Допустим, вам нужна пара функций (x, y)

Это "псевдо" язык lisp:

(function pair x y = 
   lambda(pick) 
      if pick = 1 return x 
      else return y  )

В этом примере показана функция, которая возвращает лямбда-функцию, которая ожидает параметр.

(function pi this-is-pair = this-is-pair 1)

this-is-pair должна быть построена с функцией пары, следовательно, параметр является функцией, которая ожидает другой параметр (выбор).

И теперь вы можете проверить то, что вам нужно

(pi (pair x y ) ) should return x

Я настоятельно рекомендую вам посмотреть это видео о составные данные. Большинство примеров сделаны на lisp, но понимать такую ​​концепцию полезно.

person Alan    schedule 19.05.2017

arrow_upward
0
arrow_downward

Пары или кортежи описывают предметную область товаров, представляют собой объединение всех элементов множества A и всех элементов множества B:

A × B = { (a, b) | a ∈ A, b ∈ B }

Здесь A и B являются разными типами, поэтому, если вы, например, находитесь в языковой программе, такой как C, Java, у вас может быть пара, например (String, Integer), (Char, Boolean), (Double, Double)

Теперь функция π1 — это просто функция, которая принимает пару и возвращает первый элемент, эта функция обычно вызывается в first, и вот как она выглядит в π1(x, y) = x, с другой стороны, у вас есть вторая, делающая то же самое, но возвращающая второй элемент:

fst(a, b) = a
snd(a, b) = b

Когда я изучал подпись "Характеристики языков программирования" в колледже, наш профессор порекомендовал это book, см. главу Домен продукта, чтобы понять ну это все понятия.

person Damián Rafael Lattenero    schedule 19.05.2017