[Python] un bel dilemma

[Michele Orru`]

enrico franchi <enrico.franchi a gmail.com> writes:

> Non sono certo di avere compreso la domanda.
Mi associo ad enrico sul dubbio. 

>  Come nota a margine, l'operatore di cui parli (fix) sembra proprio il
> combinatore Y.
Già. In realtà la questione è più profonda.
Perdonate il tecnicismo e gli eventuali strafalcioni, spero l'importanza
del risultato riassunto compensi ad entrambi. 

Sia U il tuo universo, su cui hai definito delle regole di riduzione
  R ⊂ (P_fin(U) × U)
dove P_fin(U) ⊂ P(U) è l'insieme delle parti *finite* di U.

Sia Ř(X): P(U) → P(U): X ↦ {y | x₁, x₂, …, xₙ / y ∈ R  con xᵢ ∈ X}
l'insieme di stati raggiungibili mediante regole di riduzione con input
in X.

Identifichiamo con Řⁱ l'i-esima applicazione di Ř, ossia l'insieme di
stati raggiungibili applicando al più i volte le regole di riduzione.

È possibile dimostrare (Knaster-Tarski) che Ř ammette un minimo punto
fisso, e che esso è
  fix(Ř) = U_i Řⁱ(∅)

Pertanto, una *derivazione* è un elemento del punto fisso di Ř, e tutte
le riduzioni che fai per eseguire un programma non sono altro che la
ricerca di un punto fisso.
Per questo quella pagina dice che è così importante dal punto di vista
teorico. Per questo la domanda di Nadir è un po' confusa.

Per chi cercasse riferimenti, io avevo appreso queste cose da pagina 52
in poi del Winskel. 
<http://gen.lib.rus.ec/book/index.php?md5=52621c8c571f29d0299aa9e8091b691f>


> 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.
Qualcuno è riuscito pure ad implementarlo sul typesystem di ghc, per una
qualche ottimizzazzione del type-checker(?); questo è il riferimento più
appropriato che ho trovato:
<https://mail.haskell.org/pipermail/haskell/2006-September/018497.html>

-- 
µ.