2016-04-22 4 views
3

ОК, поэтому я пытаюсь реализовать basics of lambda calculus. Вот оно.лямбда-исчисление в scala

Мои номера:

def zero[Z](s: Z => Z)(z: Z): Z = z 
def one[Z](s: Z => Z)(z: Z): Z = s(z) 
def two[Z](s: Z => Z)(z: Z): Z = s(s(z)) 

Частично (на самом деле, не) применяется вариант них то вроде этого:

def z[Z]: (Z => Z) => (Z => Z) = zero _ 

Прежде чем продолжить, я определить некоторые типы:

type FZ[Z] = Z => Z 
type FFZ[Z] = FZ[Z] => FZ[Z] 

Изобразительное, succ функция идет как (заказ заявки должен быть ровно вот так! Я принял определение here):

def succ[Z](w: FFZ[Z])(y: FZ[Z])(x: Z): Z = y((w(y))(x)) 

И Непримененную версию этого становится так страшно, как:

def s[Z]: FFFZ[Z] = successor _ 

Просит прощения, вот недостающие типы:

type FFFZ[Z] = FFZ[Z] => FFZ[Z] 
type FFFFZ[Z] = FFFZ[Z] => FFFZ[Z] 

Но Я застрял в функции add. Если соответствовали типам и определения (взятая here а) он идет как

def add[Z](a: FFFFZ[Z])(b: FFZ[Z]): FFZ[Z] = 
    (a(s))(b) 

Но я хочу a быть общее число типа FFZ[Z].

Так как я могу определить дополнение?

+0

Моя первая догадка, что он работает только для нетипизированного лямбда-исчисления, где значение просто * somehting *, а функция - это отображение от * something * к * something *, поэтому я могу вызвать функцию 'f', тип аргумента которой, скажем,' a: Z -> Z', и это может не соответствовать точно t o функция 'f ': (Z -> Z) -> (Z -> Z)' Я применяю ее. – zapadlo

+0

Возможно, название «Дополнение для церковных цифр в Скале» было бы более точным. –

ответ

2

В Scala можно реализовать церковные цифры. Вот одна такая довольно прямолинейная реализация:

object ChurchNumerals { 

    type Succ[Z] = Z => Z 
    type ChNum[Z] = Succ[Z] => Z => Z 

    def zero[Z]: ChNum[Z] = 
    (_: Succ[Z]) => (z: Z) => z 

    def succ[Z] (num: ChNum[Z]): ChNum[Z] = 
    (s: Succ[Z]) => (z: Z) => s(num(s)(z)) 

    // a couple of church constants 
    def one[Z] : ChNum[Z] = succ(zero) 
    def two[Z] : ChNum[Z] = succ(one) 

    // the addition function 
    def add[Z] (a: ChNum[Z]) (b: ChNum[Z]) = 
    (s: Succ[Z]) => (z: Z) => a(s)(b(s)(z)) 

    def four[Z] : ChNum[Z] = add(two)(two) 

    // test 
    def church_to_int (num: ChNum[Int]): Int = 
    num((x: Int) => x + 1)(0) 

    def fourInt: Int = church_to_int(four) 

    def main(args: Array[String]): Unit = { 
    println(s"2 + 2 = ${fourInt}") 
    } 
} 

компилирует и гравюры:

$ scala church-numerals.scala 
2 + 2 = 4 

Если бы я объяснить Чёрч с нуля Я хотел бы добавить еще комментарии. Но принимая во внимание контекст, я не уверен, что комментировать в этом случае. Пожалуйста, не стесняйтесь спрашивать, и я добавлю больше объяснений.

+0

Это красиво. Благодарю. – zapadlo

2

Я закодировал цифры, булевы и пары: https://github.com/pedrofurla/church/blob/master/src/main/scala/Church.scala следующий стиль церкви.

Одна вещь, которую я заметил, заключается в том, что использование синтаксиса функции curries было намного проще, чем использование нескольких списков аргументов.Некоторые из интересных фрагментах

type NUM[A] = (A => A) => A => A 
def succ [A]: NUM[A] => NUM[A] = m => n => x => n(m(n)(x)) 
def zero [A]: NUM[A] = f => x => x 
def one [A]: NUM[A] = f => x => f(x) 
def two [A]: NUM[A] = f => x => f(f(x)) 
def three [A]: NUM[A] = f => x => f(f(f(x))) 
def plus [A]: (NUM[A]) => (NUM[A]) => NUM[A] = m => n => f => x => m(f)(n(f)(x)) 

Теперь для их печати (очень похоже на решение Antov Трунов в):

def nvalues[A] = List(zero[A], one[A], two[A], three[A]) 

val inc: Int => Int = _ + 1 
def num: (NUM[Int]) => Int = n => n(inc)(0) 
def numStr: (NUM[String]) => String = n => n("f (" + _ + ") ")("z") 

Некоторые выход:

scala> println(nvalues map num) 
List(0, 1, 2, 3) 

scala> println(nvalues map numStr) // Like this better :) 
List(z, f (z) , f (f (z)) , f (f (f (z))))