tag:blogger.com,1999:blog-62801709543260230032024-07-01T15:01:54.220+02:00Se Programmo...Mathematics, logic, physics and proof of realityJulio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.comBlogger15125tag:blogger.com,1999:blog-6280170954326023003.post-32880702582902510932024-06-29T15:19:00.002+02:002024-07-01T15:01:16.428+02:00Turing machines vs computation
<< Dependent type theories that are total and have a computable normalization procedure
are Turing-incomplete. This is a theorem, not an opinion. Now, what the implications
are for practical usability of dependent type theories that are total, that is an entirely
different matter. >> [1] (slightly adapted: see the entire discussion for background)
Conversely, I would Julio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-89117283241391493242024-05-20T13:35:00.005+02:002024-05-20T23:22:38.104+02:00A Solution to Epimenides' Paradox
<< 'Morning everybody,
"Epimenides lies iff everybody lies!" which
I am taking to be the predicative version of
the uncooperative rational player. >>
Presentation and formal development (in Coq):
https://gist.github.com/jp-diegidio/f9a18bb0a8c87d585b1d56458cd082f6
[1] Wikipedia, "Epimenides paradox"
https://en.wikipedia.org/wiki/Epimenides_paradox
[2] Julio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-46804163451126907732024-01-21T15:24:00.006+01:002024-05-20T14:48:56.283+02:00On the logic of "it"# On the logic of "it" - Sparse (hopefully-)not-so-metaphysical thoughtsThe idea of a Characteristica Universalis, i.e. an encyclopedic compendium of *acquired knowledge* in terms of a universal formal *language* that is potentially able to express all *understanding*, becomes in our times the inverse idea that *language* encapsulates all there is to *understanding* (whence e.g. the idea/hope Julio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-56947291941699344992023-10-09T03:10:00.006+02:002024-05-20T15:01:07.884+02:00A Solution to Bertrand's ParadoxQuoting from Wikipedia, "Bertrand paradox (probability)" [1]
(there is also a nice explanation by 3blue1brown in [2]):
<< "Consider an equilateral triangle inscribed in a circle. Suppose a chord of the circle is chosen at random.
What is the probability that the chord is longer than a side of the triangle?" >>
<< The argument is that if the method of random selection Julio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-84709312020461600622023-08-07T15:23:00.001+02:002023-10-09T03:13:15.802+02:00Manifesto of LogicManifesto of Logic (v1.1-alpha)
============================
Formal Logic <-> Symbolic Logic.
Conversely, there we have the written
point of articulation between reading
and writing: from constructive logic [*],
entailing the closure of mathematics [**],
up to and including its own self-closure
by Univalence [***].
[*] The/a formalization is (in) Coq.
Proof inductive by it can answer allJulio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-56180164638812740932016-08-27T16:53:00.004+02:002023-08-07T15:23:20.898+02:00Nan.Numerics.Prime (in Prolog)Nan.Numerics.Prime/Prolog 1.2.2-betaNan.Numerics.Prime
A simple prime number library
Copyright 2016 Julio P. Di Egidio
Licensed under GNU GPLv3.
http://julio.diegidio.name/Projects/Nan.Numerics.Prime/
https://github.com/jp-diegidio/Nan.Numerics.Prime-Prolog/
library(nan_numerics_prime)
Module prime provides predicates to test (positive integer) numbers for
primality, find divisors and factor Julio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-50542492660553779162015-09-16T02:13:00.003+02:002023-11-09T13:21:15.661+01:00Answer Sources: from Fluents to Interactors[
NOTE: Meanwhile this has evolved into an open project available here:
https://github.com/jp-diegidio/Nan.System.Sources-Prolog
]
This is a follow-up to my previous post "Answer Sources in Prolog (SWI) - Preview" [1]. Here I present the flow diagram for the worker loop with support for the return operation. Implementation of the return operation upgrades our answer sources from fluents Julio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-41938432506668059162015-09-03T16:41:00.000+02:002015-09-16T02:13:47.912+02:00Answer Sources in Prolog (SWI) - PreviewI have implemented an initial version of Answer Sources in SWI-Prolog [1], now submitted for preliminary discussion to comp.lang.prolog [2]. For the rationale and design, I have followed Paul Tarau on "fluent sources" [3], although with some important differences.
[1] Code preview with answer sources and the basic combinators:
https://gist.github.com/jp-diegidio/2914cac8b5cfb2b6a95e
[2] (Julio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-81194595793351386052015-07-15T16:45:00.002+02:002024-01-19T13:39:28.502+01:00Symmetric Twins Paradox[
WARNING: This take of mine is wrong and rather reflects my own initial misunderstanding of Einsteinian relativity. Indeed, try and do the calculations! I am leaving it here as it might reflect some common mistakes made when seeing Einsteinian relativity for the first time. I might make it into a proper introductory article at some point...
]
[
ADDED: Meanwhile, a correct (AFAICT) first Julio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-84813935341663150352015-01-30T18:43:00.000+01:002015-01-30T19:48:45.835+01:00The day we discovered negatronsIt happened on sci.physics...
https://groups.google.com/d/msg/sci.physics/gIwxbAAS3Oo/SOSciNNwtU8JJulio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-17650480661997989972014-02-26T02:48:00.000+01:002015-01-30T20:03:53.781+01:00Hilbert's impossible hotel"Consider a hypothetical hotel with a countably infinite number of rooms, all of which are occupied. [...] Suppose a new guest arrives and wishes to be accommodated in the hotel. Because the hotel has infinitely many rooms, we can move the guest occupying room 1 to room 2, the guest occupying room 2 to room 3 and so on, and fit the newcomer into room 1." (*)
But we can prove that, if the hotelJulio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com1tag:blogger.com,1999:blog-6280170954326023003.post-32410325798011193912010-08-26T02:13:00.000+02:002015-09-03T16:46:09.231+02:00Se programmo...Professional, un-professional, de-professional, re-professional.
Otherwise, the ins and outs of the pros and cons.
Publicly private.
Bah, intanto lei dorme.Julio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-36818858178238008362009-07-10T01:16:00.001+02:002023-11-26T00:32:39.937+01:00A semantic space-dimension for the WebHow to give a *sensible* space-dimension to the Web.
This is an open project.
Discussion at:
"A space-dimension to the Web: a combinatorial optimisation problem"
http://groups.google.com/d/topic/sci.math/LNI4DAvSRes/discussion
=== Setting:
Let G be a weighted, directed graph.
Let S be a lattice space for G.
Let M be a physical model for G.
Let U be (the absolute value of) the potential energyJulio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-786011672811714192008-03-11T10:21:00.000+01:002015-09-03T16:49:29.381+02:00Radical contradictionTechnically speaking,
We have blown up the "root of contradiction" with an _atomic_ bomb.
To the casual philosophers we are, I will show the links below.
To the professional programmer: a crack is not a hack, but a hack is a crack.
Keep up the go(o)d work.
==============================================
Julio Di Egidio
Re: Question about proof by contradiction
Posted: Mar 10, 2008 11:12 AM
Julio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0tag:blogger.com,1999:blog-6280170954326023003.post-77902708561132665332008-03-09T16:42:00.000+01:002015-09-03T16:50:20.119+02:00The unified theory of all we can do with it (seriously)I have posted the following message to the Mathforum yesterday at 4:43 AM (GMT+00). Starting from around 6:00 AM today, the Mathforum has become less and less responsive, until at 8:00 AM it has finally stopped working.
I am reposting the message here (untouched), because at the moment it doesn't appear in any other publicly available sci.math repository.
I have also attached an exchange with Julio Di Egidiohttp://www.blogger.com/profile/11540195413991358140noreply@blogger.com0