Funkcja, która stosuje swój argument do samego siebie?

Question

Rozważmy następującą funkcję SML:

fn x => x x 

To daje następujący błąd (standardowa ml New Jersey v110.72):

stdIn:1.9-1.12 Error: operator is not a function [circularity] 
    operator: 'Z 
    in expression: 
    x x 

mogę rodzaju zobaczyć, dlaczego to nie jest mile widziane - - po pierwsze, nie jestem pewien, jak zapisać, jaki byłby jego typ - ale nie jest to całkowicie bezsensowne; na przykład mogę przekazać mu funkcję tożsamości i odzyskać ją.

Czy istnieje nazwa tej funkcji? (Czy istnieje sposób wyrażenia tego w SML?)

Answer 1

Nie ma sposobu, aby wyrazić tę funkcję w języku z systemem typu ML. Nawet z funkcją identyfikacji nie działałaby, ponieważ pierwsze x i drugie w x x musiałyby być różnymi instancjami tej funkcji, odpowiednio typu (_a -> _a) -> (_a -> _a) i _a -> _a, dla pewnego typu _a.

W rzeczywistości, układy typu przeznaczone są do zakazania konstrukcji jak

(λx . x x) (λx . x x) 

w lambda bez typu rachunku. W dynamicznie wpisany schematu językowego, można napisać tę funkcję:

(define (apply-to-self x) (x x)) 

i uzyskać oczekiwany rezultat

> (define (id x) x) 
> (eq? (apply-to-self id) id) 
#t 

Answer 2

Funkcje takie jak ten są często spotykanych w kombinatorów stałoprzecinkowych. na przykład jedna forma z Y combinator jest napisana λf.(λx.f (x x)) (λx.f (x x)). Kombinatory o ustalonym punkcie są używane do implementacji ogólnej rekursji w nietypowym rachunku lambda bez żadnych dodatkowych konstruktów rekursywnych, i jest to część tego, co tworzy niezaszyfrowany rachunek lambda Turing-complete.

Kiedy ludzie opracowali simply-typed lambda calculus, który jest naiwnym statycznym systemem typu na szczycie rachunku lambda, odkryli, że nie można już pisać takich funkcji. W rzeczywistości nie można wykonać ogólnej rekursji w prostym typie rachunku lambda; dlatego też prosty rachunek lambda nie jest już Turing-complete. (Interesującym efektem ubocznym jest to, że programy po prostu wpisany lambda rachunku zawsze zakończyć.)

rzeczywistym statycznie wpisywanych języków programowania, takich jak konieczność Standardowy ML wbudowanym mechanizmom rekurencyjnych w celu przezwyciężenia tego problemu, takie jak nazwy funkcji rekurencyjnych (zdefiniowane jako val rec lub fun) i nazwane rekursywnymi typami danych.

Nadal można używać rekurencyjnych typów danych do symulacji czegoś, co się chce, ale nie jest tak piękne.

Zasadniczo chcesz zdefiniować typ, taki jak 'a foo = 'a foo -> 'a; jest to jednak niedozwolone. Zamiast tego zawinąć go w typ danych: datatype 'a foo = Wrap of ('a foo -> 'a);

datatype 'a foo = Wrap of ('a foo -> 'a); 
fun unwrap (Wrap x) = x; 

Zasadniczo Wrap i unwrap są wykorzystywane do transformacji między 'a foo i 'a foo -> 'a, i vice versa.

Kiedy trzeba wywołać funkcję na sobie, zamiast x x, musisz jawnie napisać (unwrap x) x (lub unwrap x x); tj. unwrap przekształca go w funkcję, którą można następnie zastosować do pierwotnej wartości.

P.S. Inny język ML, OCaml, ma opcję włączania typów rekurencyjnych (zwykle wyłączone); jeśli uruchamiasz interpreter lub kompilator z flagą -rectypes, możliwe jest pisanie takich rzeczy, jak fun x -> x x. Zasadniczo, za kulisami, sprawdzanie typu określa miejsca, w których należy "zawinąć" i "rozwinąć" typ rekursywny, a następnie wstawia je dla ciebie. Nie jestem świadomy żadnej standardowej implementacji ML, która ma podobne funkcje typów rekursywnych.