<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">2015-07-28 18:57 GMT+01:00 Nadir Sampaoli <span dir="ltr"><<a href="mailto:nadirsampaoli@gmail.com" target="_blank">nadirsampaoli@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">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.: <a href="https://en.m.wikibooks.org/wiki/Haskell/Fix_and_recursion" target="_blank">https://en.m.wikibooks.org/wiki/Haskell/Fix_and_recursion</a></p>
<p dir="ltr">Oppure no?</p></blockquote></div>Non sono certo di avere compreso la domanda. </div><div class="gmail_extra"><br></div><div class="gmail_extra">Facciamo un passo indietro e stiamo nel mondo della teoria della calcolabilita'.</div><div class="gmail_extra">Abbiamo una prima categoria di funzioni, note come "primitive ricorsive" che sono quelle costruibili con le seguenti operazioni:</div><div class="gmail_extra"><br></div><div class="gmail_extra">Uso una sintassi similpython, ma ricorda che il dominio e' solo N: non ci sono numeri negativi.</div><div class="gmail_extra"><br></div><div class="gmail_extra">1. constante: lambda: 0</div><div class="gmail_extra">2. successore S: lambda n: n+1</div><div class="gmail_extra">3. proiezioni:</div><div class="gmail_extra">    lambda i, *args: args[i]</div><div class="gmail_extra">    (in effetti hai una proiezione per ogni arita' n di args ed i e' assunto essere < n)</div><div class="gmail_extra">4. composizione:</div><div class="gmail_extra">    lambda f, *gs: lambda *args: f(*[g(*args) for g in gs])</div><div class="gmail_extra">5. ricorsione primitiva (qui esco da Python se no divento stronzo a scriverla giusta...)</div><div class="gmail_extra">     </div><div class="gmail_extra">    h(0, *x) = g(*x)</div><div class="gmail_extra">    h(S(n), *x) = g(n, h(n, *x), *x)</div><div class="gmail_extra"><br></div><div class="gmail_extra">Ora tutte le funzioni che costruisci a partire da la sopra sono primitive ricorsive e sono *totali*.</div><div class="gmail_extra"><br></div><div class="gmail_extra">Su questo, se aggiungi la mu-ricorsione (<a href="https://en.wikipedia.org/wiki/%CE%9C-recursive_function">https://en.wikipedia.org/wiki/%CE%9C-recursive_function</a>) 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.</div><div class="gmail_extra"><br></div><div class="gmail_extra">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.</div><div class="gmail_extra"><br></div><div class="gmail_extra"> Come nota a margine, l'operatore di cui parli (fix) sembra proprio il combinatore Y.</div><div class="gmail_extra">Questa e' la faccia di Y in Python: <a href="http://www.enrico-franchi.org/2008/10/y-combinator-in-python.html">http://www.enrico-franchi.org/2008/10/y-combinator-in-python.html</a></div><div class="gmail_extra">O per lo meno, una delle facce.</div><div class="gmail_extra"><br></div><div class="gmail_extra"><br></div><div class="gmail_extra"><div><br></div>-- <br><div class="gmail_signature"> .<br>..: -enrico-</div>
</div></div>