Lambda Calculus: создайте функцию, которая принимает больше аргументов с каждой итерацией

Question

Я пытаюсь построить функцию, которая принимает заданное количество аргументов и всегда возвращает одно и то же значение.

Это часть домашней работы. Существует намек при условии:

"К-полосная Т" это функция, которая принимает K аргументы и всегда возвращает T. А "0-полосная T" просто Т.

Где к предоставляется как церковная цифра, а T - выражение лямбда для True (\ x. \ yx).

Полная задача - предоставить выражение лямбда, которое вычисляет функцию k-way ИЛИ. Где число аргументов «boolean» предоставляется перед аргументами «boolean». например:

((OR 3) F T F) 

Но сейчас я пытаюсь создать что принимает к аргументы и всегда возвращает T. В качестве первого аргумента представлен k.

((TRUE 2) T F) == T 

Поэтому в основном я wan't создать функцию, которая имеет еще один аргумент для каждой церкви числительное «итерационного».

Но почему-то я полностью застрял.

Могу ли я сделать это только с церковной цифрой? Или мне нужна рекурсия (Y-Combinator)?

В целом: Есть ли хорошие инструменты (например, для визуализации), которые поддерживают создание лямбда-выражений.

Я действительно удивлен силой исчисления лямбда, и я действительно хочу ее изучить. Но я не знаю, как ...

Заранее спасибо

Answer 1

я покажу, как реализовать функцию TRUE. Поскольку k не фиксирован, вам нужен комбинатор с фиксированной запятой (Y, но это не единственный комбинатор с фиксированной запятой). Прежде всего пару слов об обозначениях, которые я использовал ниже: iszero (берет цифру церкви, проверяет, является ли она церковной нолью и возвращает церковь boolean), T (истинное логическое значение, закодированное Церковью), pred (предшественник для церковных цифр) и Y (комбинатор с фиксированной запятой).

let TRUE = Y (λr. λn. (iszero n) T (λx. (r (pred n)))) 

Обратите внимание, что let не является частью синтаксиса лямбда-исчисления, это metasyntax ввести имя (для нас).

Это работает следующим образом: Yрода преобразует r аргумент в «Я» - когда функция вызывает r она называет себя.Чтобы проиллюстрировать это, я переписал бы это в рекурсивную форму (предупреждение: это только для иллюстративных целей, лямбда-исчисление не позволяет, так как все функции анонимны, вы не можете их назвать, используя их имена - нет никакого способа для этого):

let TRUE = λn. (iszero n) T (λx. (TRUE (pred n))) 

Я снял с λr. часть и заменить r на TRUE (опять же, пожалуйста, не делайте это в вашей домашней работы, она не действует лямбда-исчисление).

И это определение будет легче понять: если TRUE называется как этот TRUE 0 он просто возвращает T, в противном случае она возвращает функцию одного аргумента, который оборачивается вокруг функции (п - 1) аргументы, по сути представляющий собой функцию n аргументов.

Что касается вашего вопроса о инструментах: один из способов - использовать схему/ракетку - это поможет проверить, что ваш «код исчисления лямбда» работает так, как должен. Например, вот реализация TRUE в Ракетка:

(define (Y f) 
    ((lambda (x) (x x)) 
    (lambda (x) (lambda (a) ((f (x x)) a))))) 

(define TRUE 
    (Y (lambda (r) 
     (lambda (n) 
     (if (zero? n) 
      #t 
      (lambda (x) (r (sub1 n)))))))) 

;; tests 
> (TRUE 0) 
#t 
> ((TRUE 1) #f) 
#t 
> (((TRUE 2) #f) #f) 
#t 
> ((((((TRUE 5) #f) #f) #f) #f) #f) 
#t 

Я должен добавить, что я использовал здесь встроенный в булевы, целые числа, если выражение, sub1, zero? вместо церковно-закодированных них. В противном случае это сделало бы этот пример намного большим (или неполным).