Esiste un algoritmo pratico / struttura dati che non può essere fatto con il Lambda Calculus non ricorsivo aumentato con foldl?

Question

Esiste un algoritmo pratico / struttura dati che non può essere fatto con il Lambda Calculus non ricorsivo aumentato con foldl?

#1 da (7 voti)

1

Nella mia ricerca di un pratico linguaggio di programmazione completo non-turing, ho prestato attenzione al lambda-calcolo con auto-applicazione non consentita - cioè, x x vietato. Dopo aver preso quella lingua e aumentata con le liste e le operazioni foldl e range , praticamente qualsiasi algoritmo che ho provato finora è implementabile. È banale implementare filter , reverse , head , tail , map , scanl , zip e molti altri - foldl sostituisce la necessità di ricorsione.

Riesci a pensare ad un algoritmo pratico e importante che sarebbe annullabile in quella lingua?

It is no coincidence that all of them use self-application—the application of an expression to itself. It is through self-application that repetitive computation can be simulated in the lambda calculus. Indeed, the third of the previous three examples is famous because it can encode recursive function deﬁnitions.

Da link .

programming-languages functional-programming data-structures lambda

posta MaiaVictor 27.12.2013 - 12:27

fonte

1 risposta

Leggi altre domande sui tag programming-languages functional-programming data-structures lambda

Come creare un prototipo di metodo Python Quale è meglio: per la lunghezza del buffer valida?

score 7 · Accepted Answer

tl; dr (o non so cos'è un combinatore Y)

Questa domanda si basa sul presupposto che il linguaggio sopra definito non è completo di Turing, in realtà è completo di Turing e quindi la domanda non è valida - tutti gli algoritmi possono essere espressi nella lingua definita sopra come è il significato di Turing -completeness.

Ok. Bene a quanto pare questo deve essere esplicitamente scritto.

La dimostrazione della completezza di turing segue banalmente da una ricorsione illimitata che può essere derivata da un combinatore di punti fissi.

Nota il tradizionale combinatore Y

Y f = (\x -> f (x x)) (\x -> f (x x))

Definisci

cons = \a b f -> f a b
car  = \x y -> x
cdr  = \x y -> y

fst  = \p -> p car
snd  = \p -> p cdr

Questa è solo la codifica standard delle coppie di chiese.

nil = \x -> x -- Or anything really
fold = \x -> cons x nil
unfold = \x -> fst x

Poi

Y f = (\x -> f (unfold x x)) (fold (\x -> f (unfold x x)))

Nessuna applicazione autonoma, ma codifica ancora correttamente il combinatore Y. In precedenza l'ho scritto in Haskell. C'è fold e unfold richiedono più jiggery-pokery a causa dei tipi, ma dato che lambda calcolo non ne ha nessuno possiamo tranquillamente ignorarlo:)

Abbiamo appena dimostrato di avere una lingua completa di Turing. Ogni algoritmo è quindi esattamente efficiente quanto può essere codificato in un Lambda Calculus. Ciò invalida anche la premessa originale della domanda secondo cui la lingua è Turing-incompleta.