Правильный способ определения конструкторов лямбда-исчисления

Есть ли четкий способ найти термины в лямбда-исчислении? Например, предположим, что у нас есть конструктор пары

pair = λa. λb. λf. f a b

и у нас есть конструктор fst

fst = λp. p (λa. λb. a)

который возвращает первый элемент пары, теперь мы должны определить конструктор snd, который возвращает второй элемент пары. Я пришел, чтобы определить это так

snd = λp. p (λa. λb. b) с snd (pair a b) = b.

snd можно определить также как

snd = λp. p (λb. λa. b) ,

вопрос в том, есть ли четкий способ определения новых конструкторов?

Как человек должен думать, когда мне нужно определить конструкторы, и как я могу проверить правильность моего ответа, когда меня просят определить новые конструкторы.


typed-lambda-calculus lambda-calculus
person Gallaoui    schedule 21.08.2018    source источник
comment
ваш вопрос на самом деле довольно расплывчатый и широкий, поэтому, если у вас есть какие-то конкретные проблемы, не стесняйтесь уточнить их.   -  person Will Ness    schedule 29.08.2018
comment
привет, Уилл Несс, я знаю, что это широкий вопрос, у меня нет чего-то конкретного, все, что я хочу знать, есть ли лучший способ или что-то, о чем я должен позаботиться при определении новых конструкторов и как я могу быть уверен, что мой новый конструктор определяется правильно, я думаю, что ваша идея писать определения в комбинаторном стиле - хороший способ, большое спасибо   -  person Gallaoui    schedule 31.08.2018
comment
рад был помочь. не стесняйтесь задавать дополнительные вопросы. счастливых дорог!   -  person Will Ness    schedule 31.08.2018

Ответы (1)


arrow_upward
1
arrow_downward 

(λa. (λb. b)) x y = (λb. b) y = y

но

(λb. (λa. b)) x y = (λa. x) y = x

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

Имена не учитываются, за исключением установления соответствия с аргументами. Количество позиций аргументов.

Что касается того, как об этом думать, я часто нахожу, что запись определений в комбинаторном стиле намного проще для понимания:

pair a b selector = selector a b

fst apair = apair first_argument_selector

snd apair = apair second_argument_selector

first_argument_selector  a b = a

second_argument_selector a b = b

Я думаю, это очень ясно. "Пара a и b, при заданной процедуре селектора, сначала подаст a, а b – второе" и т. д.

Мы можем переключаться между двумя стилями с помощью простых синтаксических преобразований, например:

second_argument_selector     a     b = b       =>
second_argument_selector     a = (λb . b)      =>
second_argument_selector = (λa . (λb . b))

Часто очень полезен принцип принятия желаемого за действительное: мы используем некоторые функции так, как если бы они уже были написаны; тогда их использование диктует нам, как они должны быть определены. Точно так же, как мы сделали с first_argument_selector и second_argument_selector выше.

Хорошие имена помогают. Визуальное выравнивание кода помогает. Кроме того, используя полные скобки (как я сделал в верхней части поста).

person Will Ness    schedule 29.08.2018