>>>>> "t" == tbanelwebmin <tbanelweb...@free.fr> writes:
t> - If I understand, a cell is either a string or a lazy closure able to
t> compute it. - As soon as the value of a cell is needed, the closure is
t> computed. - The closure is discarded and replaced by the sound string
t> value, ensuring any closure is computed only once.
Yes, this describes what happens inside the `loeb` computation rather well.
>From the users perspective, it is a mapping from:
matrix of (matrix of strings -> string)
->
matrix of string
The use of lazy evaluation to ensure that only needed cells are computed, and
only then computed once, is an effective implementation strategy. Since we
will be rendering the final matrix back into a table, then of course every
cell is going to be needed, but the majority of cells won’t refer to the
incoming matrix parameter and will just be constant strings.
t> Löb's theorem states that in Peano arithmetic (PA) (or any formal system
t> including PA), for any formula P, if it is provable in PA that "if P is
t> provable in PA then P is true", then P is provable in PA.
If I take my function type above and replace “matrix of” with any functor, I
get:
Functor f => f (f a -> a) -> f a
And if the "functor“ happens to be, say, a provability modality in modal
logic, then:
□ (□ P → P) → □ P
And we have recovered Löb! :-)
--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2
Sponsor my open source on github.com/sponsors/jwiegley or patreon.com/jwiegley
