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 e.g. 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^$2 <>= T` ?
What does this expression *mean*: `2` ?

Sure, we might *explain* each of those, but as long as the explanation is itself formal, we still need to find a bottom to 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 "can-/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.

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

So, I think Leibniz's formal-encyclopedic project is by now doable, with applications potentially up to the legal context.  On the other hand, and exactly for reasons of concreteness and applicability, I do *not* think *we* can get away without the umbrella of a (trustless, hopefully) *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 correct answer, which happens to be 1/3.

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 - first part https://youtu.be/pJyKM-7IgAU?si=T_CcTuX42Qqna6Rt - second part

Monday 7 August 2023

Manifesto of Logic

Manifesto 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 all
questions that can be logically asked.
Equivalently, by Curry-Howard.
[**] ToA = the Theory of All (we can do with it).
[***] ToT = the Theory of That (we can talk about).

Saturday 27 August 2016

Nan.Numerics.Prime (in Prolog)

Nan.Numerics.Prime/Prolog 1.2.2-beta
Nan.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 numbers, generate prime numbers in some
interval, find consecutive prime numbers, and save/load all prime numbers
up to some value to/from a file or stream.

Implements a variant of the Miller-Rabin primality test that is
deterministic for numbers up to 3317044064679887385961980, otherwise
it is probabilistic with the number of iterations fixed at 20.

NOTE: Since the primality test in use is probabilistic in general, this
library is not suitable for cryptographic applications.

See the README file for more details.

This library was developed and tested with:
SWI-Prolog 7.3.25 - http://www.swi-prolog.org/

Wednesday 16 September 2015

Answer 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 [2] to interactors [3].
[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

[ 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 approach is here:
Special Relativity: Inertial Frames ]

MinkScale2
In the context of special relativity, we present a twins experiment that is symmetric between the twins, so that a paradox appears inescapable, in the form of a violation of the principle of causality.

Here is the experiment (we would argue that effects of acceleration can be made arbitrarily small in our setup):

  == The twins, call them L and R, are each given a clock at birth and get the clock fixed to their body: the two clocks have been previously synchronised.  Assume, for simplicity, that the common origin of space-time for the clocks is set to the moment and place of the twins' birth, as well as a common choice of coordinates is made, such that the twins, at that very moment, share the same frame of reference (up to arbitrary precision).
     Just after birth, the twins (with their clocks) are each embarked on a rocket.  Assume collinear motion for simplicity.  The two rockets start in opposite direction relative to the origin, carrying L and R respectively.  The plan is for the rockets to fly away from each other at some fixed (appropriately high) constant speed for some fixed (appropriately long) proper time, then simply invert course and fly back at opposite speed to the point of origin (in space), and stop there.  (Effects of acceleration can be minimised by making the total proper time the rockets are subject to acceleration appropriately small relative to the total proper time of the journey.)
     The twins at that point rejoin, again sharing a common frame of reference (up to arbitrary precision).  We ask what the two clocks measure for each twin in this common frame. ==

To compute results, we apply special relativity.  (We advise readers go through this little but essential exercise by themselves.)  We find that R's clock looks late (i.e. back in time) to L, but, *at the same time* (twins and clocks are in a common frame of reference), L's clock looks late to R!  This conclusion is an inescapable consequence of the theory, and now the problem becomes how to make sense of these results.  In fact, since all clocks are affected, including the biological ones, at the end of the journey each twin effectively finds the other younger than himself: then, per *reciprocity* (causality), i.e. that in the same frame of reference, if I am older than you, you must be younger than me, we can argue that each twin is at the same time younger and older than the other, which is indeed absurd!

Note that the absurdity would not be so patent if we just let the two clocks travel, hence we sent the twins, too: not because the presence of the twins is necessary for relativistic effects to occur, the clocks must be late relative to each other regardless of anyone observing them, rather because only the twins can "testify" that the conclusion of the experiment, so special relativity theory, is indeed at odds with the principle of *causality*.

Bottom line: if special relativity is correct, it must be incomplete.