Saturday, 29 June 2024

Turing 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 argue that Turing Machines are not an adequate model of computation: there just is no such thing as a machine that does not halt or crash or get switched off, eventually. And, eventually rather goes with interactively.

In fact, more generally, the name of that "misunderstanding" is yet again the problem of infinity in standard mathematics and mathematical logic.

[1] SE, Proof Assistants, "Possible root cause(s) of
the misunderstanding that DTT implies not Turing complete?"
https://proofassistants.stackexchange.com/q/4002/3006#comment7782_4002

Monday, 20 May 2024

A 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] Wikipedia, "Non-cooperative game theory"
https://en.wikipedia.org/wiki/Non-cooperative_game_theory

Sunday, 21 January 2024

On the logic of "it"

On the logic of "it" - Sparse (hopefully-)not-so-metaphysical thoughts

The 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 in particular the idea/hope that so called Large Language Models are "a solution to problems").

But the simplest formalization exercise indicates that between language and understanding (or, language and "reality") there is an essential gap that only imagination can fill.

What does this expression mean: `fun x y => x + y` ?
What does this expression mean: `a^${h} <>~ T` ?
What does this expression mean: `2` ?

Sure, we might explain each of those, but, as long as the explanation is itself formal, we'd still need to find the bottom of it (what does "it" mean?).  Eventually, the problem of meaning remains at the level of our formal primitives.

And that is properly our symbolic level, the one that simply "cannot and will not be explained".  I.e. not any more than its own shape is its own diagram (or that "(its) nature is its own explanation"): ultimately, the idea/hope being, we cannot explain it but we can understand it to the point of naming it.

Incidentally, a principle is "let code speak for itself", which entails that our formal language should be as readable as natural language, just without the ambiguities, as the formal aspect exactly takes care that code cannot lie about itself (about its assumptions as well as derivations).

That much for a concrete convergence of formal and symbolic logic. Indeed, I'd propose Leibniz's formal-encyclopedic project is by now feasible, with applications potentially up to the legal context.

However, and precisely for concreteness, I think we cannot get away with it unless under a (trustless, surely) contract, where "it" takes the form of a (collaborative, hopefully) game-theoretic protocol, for "the acquisition, revision, consolidation and exercise of mutually informed and formally verified knowledge".

Monday, 9 October 2023

A Solution to Bertrand's Paradox

Quoting 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 is specified, the problem will have a well-defined solution (determined by the principle of indifference). »

« Bertrand gave three arguments (each using the principle of indifference), all apparently valid, yet yielding different results. »

« The three solutions presented by Bertrand correspond to different selection methods, and in the absence of further information there is no reason to prefer one over another; accordingly, the problem as stated has no unique solution. »

« Edwin Jaynes proposed a solution to Bertrand's paradox, based on the principle of maximum ignorance - that we should not use any information that is not given in the statement of the problem. »

No, not "determined by the principle of indifference" (and not even by one of "ignorance", if not about how to read, and write, problem statements, i.e. do not assume more than is given): rather, by definition, given any two points on a circle, we call _chord_ the straight line *segment* connecting the two points. Hence a random distribution of chords is a random distribution of pairs of points on the circle. Whence there is one and only one correct answer, which happens to be ...

Indeed, as for a logical analysis, the question is "given an arbitrary circle consider drawing random chords", not "given arbitrary lines in space consider those that are secant to a random circle".

[1] Wikipedia, "Bertrand paradox (probability)"
https://en.wikipedia.org/wiki/Bertrand_paradox_(probability)

[2] "Bertrand's Paradox (with 3blue1brown) - Numberphile" on YouTube
https://youtu.be/mZBwsm6B280?si=uXETifeOvY4S9fmI (part 1)
https://youtu.be/pJyKM-7IgAU?si=T_CcTuX42Qqna6Rt (part 2)

Monday, 7 August 2023

Manifesto of Logic

 Manifesto of Logic v1.2-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 its own self-closure by Univalence [***].

[*] The/a formalization is (in) Coq:
proof inductive by it can answer all
questions that can be logically asked.
Equivalently, by the Curry-Howard correspondence.
[**] ToA = the Theory of All (we can do with it).
[***] ToT = the Theory of That (we can talk about).

Wednesday, 16 September 2015

Answer Sources: from Fluents to Interactors

[ NOTE: Meanwhile this has evolved into an open project here:
  https://github.com/jp-diegidio/Nan.System.Sources-Prolog ]

This is a follow-up to my earlier post "Answer Sources in Prolog (SWI) - Preview" [1]. Here I present the flow diagram for the worker loop with support for the yield operation (return in Tarau's). Implementation of yield upgrades our answer sources from fluents [2] to interactors [3].

Nan.Kernel.Worker.FLOW
(click to open full size)

[1] My post, "Answer Sources in Prolog (SWI) - Preview":
http://seprogrammo.blogspot.co.uk/2015/09/answer-sources-in-prolog-swi-preview.html
[2] Paul Tarau, "Fluents: A Refactoring of Prolog for Uniform Reflection and
Interoperation with External Objects":
http://www.cse.unt.edu/~tarau/research/LeanProlog/RefactoringPrologWithFluents.pdf
[3] Paul Tarau and Arun Majumdar, "Interoperating Logic Engines":
http://www.cse.unt.edu/~tarau/research/LeanProlog/InteroperatingLogicEngines.pdf

Thursday, 3 September 2015

Answer Sources in Prolog (SWI) - Preview

I 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] (Short) presentation and discussion on comp.lang.prolog:
https://groups.google.com/d/msg/comp.lang.prolog/JToeE7Read8/sZ0xg1-cBgAJ
[3] Paul Tarau, "Fluents: A Refactoring of Prolog for Uniform Reflection
and Interoperation with External Objects":
http://www.cse.unt.edu/~tarau/research/LeanProlog/RefactoringPrologWithFluents.pdf

Wednesday, 15 July 2015

Symmetric Twins Paradox

« Indeed, try and do the calculations! »

A correct (AFAICT) first approach is here:
Special Relativity: Inertial Frames
Corollary 1: Retrocausation.
Corollary 2: Nobody understands Relativity.

[UPDATE 2024-12-19]
I have not yet found the time to approach the Twins Paradox proper, which is about finding coherence conditions for retrocausation...

Wednesday, 26 February 2014

Hilbert'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. » [1]

But we can prove that, if the hotel is full, accommodating new guests is actually impossible.

Indeed, to say that the hotel is fully is to say that, for all n in |N, room n is occupied. Thus, a fortiori, room 1 is occupied and, for all n in |N, if room n is occupied, room n+1 is also occupied. Which in turn is equivalent to saying that there is no n in |N such that room n+1 is available. Hence, no more guests can be accommodated. QED.

In other words, by the simply-inductive definition of the natural numbers (a sequence), the hotel can never be full; conversely, there can be no such thing as a hotel (a set) that is potentially infinite. Bottom line, the simply endless is just not of the same logical quality as the actually infinite. Consequently, nothing peculiar about infinite sets can be proved via plain finite induction on sequences.

[1] http://en.wikipedia.org/wiki/Hilbert's_paradox_of_the_Grand_Hotel