[Python] un bel dilemma

enrico franchi enrico.franchi a gmail.com
Mer 29 Lug 2015 13:15:27 CEST


2015-07-28 18:57 GMT+01:00 Nadir Sampaoli <nadirsampaoli a gmail.com>:

> Capisco. Ma tolte le funzioni non-totali (aka parziali) che contengono
> evidentemente un bottom, esiste anche un insieme di funzioni che pur
> essendo ben-tipizzate vanno a bottom. Es.:
> https://en.m.wikibooks.org/wiki/Haskell/Fix_and_recursion
>
> Oppure no?
>
Non sono certo di avere compreso la domanda.

Facciamo un passo indietro e stiamo nel mondo della teoria della
calcolabilita'.
Abbiamo una prima categoria di funzioni, note come "primitive ricorsive"
che sono quelle costruibili con le seguenti operazioni:

Uso una sintassi similpython, ma ricorda che il dominio e' solo N: non ci
sono numeri negativi.

1. constante: lambda: 0
2. successore S: lambda n: n+1
3. proiezioni:
    lambda i, *args: args[i]
    (in effetti hai una proiezione per ogni arita' n di args ed i e'
assunto essere < n)
4. composizione:
    lambda f, *gs: lambda *args: f(*[g(*args) for g in gs])
5. ricorsione primitiva (qui esco da Python se no divento stronzo a
scriverla giusta...)

    h(0, *x) = g(*x)
    h(S(n), *x) = g(n, h(n, *x), *x)

Ora tutte le funzioni che costruisci a partire da la sopra sono primitive
ricorsive e sono *totali*.

Su questo, se aggiungi la mu-ricorsione (
https://en.wikipedia.org/wiki/%CE%9C-recursive_function) hai un altro
cioppo di funzioni totali *non* primitive ricorsive *e* hai aperto le porte
alle funzioni parziali. Incidentalmente l'insieme delle funzioni
mu-ricorsive coincide con quello che puoi calcolare con una macchina di
turing. Nota a margine, un esempio di funzione totale che non e' primitiva
ricorsiva e' la celebre funzione di Ackermann.

Ora, se vogliamo introdurre i tipi per davvero, mi sposterei dal formalismo
del lambda calcolo (tutto sommato intuitivo) ai combinatori SKI e li sopra
puoi introdurre i tipi in modo a mio vedere piu' agevole. O per lo meno, 10
anni fa mi era sembrato piu' agevole. Puoi chiaramente anche fare il typed
lambda calculus. Ora, davvero, non ricordo molto a riguardo.

 Come nota a margine, l'operatore di cui parli (fix) sembra proprio il
combinatore Y.
Questa e' la faccia di Y in Python:
http://www.enrico-franchi.org/2008/10/y-combinator-in-python.html
O per lo meno, una delle facce.



-- 
.
..: -enrico-
-------------- parte successiva --------------
Un allegato HTML è stato rimosso...
URL: <http://lists.python.it/pipermail/python/attachments/20150729/b657f2dd/attachment.html>


Maggiori informazioni sulla lista Python