enrico franchi <enrico.fran...@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>
--
µ.
_______________________________________________
Python mailing list
Python@lists.python.it
http://lists.python.it/mailman/listinfo/python
