Showing posts with label (en). Show all posts
Showing posts with label (en). Show all posts

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 could 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 Twin 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 Twin 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 full 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

Thursday, 26 August 2010

Se programmo...

Professional, un-professional, de-professional, re-professional.

Otherwise, the ins and outs of the pros and cons.

Publicly private.

Bah, intanto lei dorme.

Friday, 10 July 2009

A semantic space-dimension for the Web

How 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 energy (in M over S, given G)

=== Problems:

Problem 1 (optional): Express U.
Problem 2 (optional): Minimize U.
Problem 3: Express and minimize U given the following constraints:

- Constraint 3.CG1: Weights in G have positive rational values.

- Constraint 3.CG2: G is sparse.

- Constraint 3.CG3: G is dynamic, i.e. nodes and edges change (appear, desappear, change their weight). The dynamic is by discrete singular events, changes are smooth.

- Constraint 3.CS1: S is a diophantine circle where positions start from zero along the circumference, and the distance function x is:

    let c be the circumference (i.e. number of nodes in G)
    let x' = x1 - x2 (absolute distance, integer >= 0)
   
    x := x'      , if x' <= c/2
         c - x'  , otherwise
    (i.e. distance along the shortest arc, integer >= 0)

- Constraint 3.CM1: Within model M, the force F is:
    let i,j be non-negative integers indexing nodes in G
   
    f_ij = k_ij * x_ij , if exists in G edge i->j with weight k_ij
           0             , otherwise
    (i.e. absolute elastic force, rational >= 0)
   
    F = sum_i sum_j f_ij
    (total force, rational >= 0)

- Constraint 3.CU1: Given that G is dynamic (see CG3), we want to minimise U and keep it minimised!

=== Solutions:

Our solution to Problem 3 at the moment consists in a "local approach".  We build a graph that is near-to-optimal (by inserting any new node at a location such to minimise the total energy change), plus we have a process that keeps iterating the configuration space for local improvements (by swapping adjacent nodes).  The idea is that this process should be able to keep up with changes (which are smooth, see 3.CG3 and 3.CU1), and this together with the strategy of insertion should be enough to keep the system (at least!) at a near-to-optimal minimum.  Simulated annealing can also be easily implemented.

Incidentally, in the setting of Problem 3 there is no role for node weights.  This is a choice, not a simplification, related to semantic considerations.  This can be discussed: we are after a *sensible* way to give a space-dimension to the Web.

Tuesday, 11 March 2008

Radical contradiction

Technically 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
http://mathforum.org/kb/message.jspa?messageID=6131405

[...]

BTW, here is an extract from a letter from Wittgenstein to Russel, 1921, which I think sheds some light (I'm

afraid I'll have to traslate, I've got it in Italian):

"I believe our problems track down to _atomic_ propositions. You'll see it if you try to precisely explain

how the Copula is such propositions has meaning. I cannot explain it and I believe that, once an exact answer

is given to this question, the problem of <> and of the apparent variable will be _much_ nearer its

solution, if not solved. Now I think above <> (the good old Socrates!)."

The good old Ludwig!!

Explaining that meaning, by means of the empty set "we" are, is indeed what I have shown (again, until dis-

proved).

Julio

==============================================

Marshall
Re: Question about proof by contradiction
Posted: Mar 10, 2008 5:46 PM
http://mathforum.org/kb/message.jspa?messageID=6131836

> >> Proof by contradiction can be formalized as
>
> >> (P -> (A and not(A))) -> not(P).
[...]
> The proof in question, in fact, does not even use proof by
> contradiction. It has the form
>
> (P -> not(P)) -> not(P).
>
> This is not a proof by contradiction.

[...]

Does anything interesting happen if we transform them somewhat?

(P -> (A and not(A))) -> not(P)
(P -> false) -> not(P).
(not(P) or false) -> not(P)
not(P) -> not(P)

Well, I seem to have destroyed the formula's essential nature
by these manipulations. How did THAT happen? Apparently
truth-value-preserving transformations don't preserve some things
that aren't truth values.

Marshall

==============================================

Sunday, 9 March 2008

The 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+0. 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 Mr Aiya-Oba, who was so kind to support in dis-closing the proof.

WARNING: MIND YOU !!
This is no fucking around, handle with care and take at your own risk!

============================

Julio Di Egidio
The unified theory of all we can do with it (seriously)
Posted: Mar 8, 2008 4:34 AM
http://mathforum.org/kb/thread.jspa?threadID=1708310

[I wish to just warn you I am not a professional in any of the fields I am going to touch, I am rather some kind of abstract logician plus a professional programmer, so please mind the step(s). What I'm after is for (dis-)proofs to the following chain of assertions. As to the "discussion", that might very well start later, and I do mean it. OTOH, questions are always welcome. Again, please mind the step(s), there are none.]

Subject: The unified theory of all we can do with it (seriously).

Freely mentioning Russell, Cantor, Goedel, Turing, Complexity, Walster, Golden, and Di Egidio.

Below, "dis-x" stands for "x and only x", where the connotations are thought to be even more interesting.

>> Walster shows[*] that a number is a set, and that the empty set is a number.

Walster extends interval arithmetic with the empty interval and intervals with one or both infinite end-points. He first defines operations on the empty interval; from there, he closes arithmetic to any operator and function combinations on the entire domain. In his system, the empty interval is dominant to any other, including the entire interval, i.e. {}.rel.X = {} and X.rel.{} = {}, for all X in IR*, for all interval relation. (More from Walster later.)

(1) We now can say: a number dis-is a set, and the empty set is dominant to any number, dis-including itself.

>> Russell asks what is the set of all sets not having themselves as elements.

(2) We now can say: the set of all sets not having themselves as elements dis-is the empty set, i.e. the paradoxical set of paradoxical sets not having any elements, dis-including themselves.

>> Cantor wanders how the diagonal argument leads to entities outside the domain.

(3) We now can say: the diagonal argument leads to the all-encompassing void of the empty set, i.e. the paradoxical number of paradoxical numbers (or, more simply, the "without" (outside) of the domain, as seen from "within" (inside) the domain).

>> Goedel proves that self-referential entities must exist, yet undecidably.

(4) We now can say: the purely self-referential set dis-is the empty set, by foundation; in fact, a progression up the chain of provability systems can be seen from "I can't be proved", to "I am not true", up to "You fail", where this last sentence dis-is the empty set and expresses the limit ad infinitum of goedelization.

Incidentally, "You fail" might express more than the abstract sentence ~Bf ("consis"; can read "not-believe-that"), where belief is the foundational meaning behind logical negation and falsehood. I cannot say (for lack of specific knowledge) what this strictly entails on the "incompleteness arguments in a general setting" (Smullyan, 1992), but the introduction of the empty set as a full fledged and foundational entity, and the closedness of algebraic systems it brings, seem to suggest a profound impact. For instance, it seems quite evident that belief should itself be founded on "us", the subjects, and aren't we, with respect to the system, just its very external domain? In a sense, ultimately, "we" are the empty set and the self-referential dis-proof of all proofs.

Indeed, OTOH, I must note that, as far as "real" systems are concerned (i.e., in any form of "engineering"), the introduction of the empty set is in itself enough to formally found our very daily "practices", where we are used to discard apparently incorrect answers (i.e., dis-answers within our accepted domain), and where we, ultimately, improve throw failure (i.e., breaking out of the boundaries of the accepted). This is in the lights of what straight follows.

>> Turing, in shades of Hilbert's tenth problem, restates the question in terms of the "halting problem".

(5) We now can say: All machines indeed stop, sooner or later; in the worst case, it is "us" (see my preceding note) stopping them, and, in any meaningful sense, the machines "we" stop have failed, and dis-belong to the void of the empty set, which happens to be the void "we" are.

In simpler terms, the set of failing machines is the set of machines that are "not machines" at all, with respect to the bounds "we" impose on the accepted domain.

Incidentally, for all this to be (believed) true, we must accept that classical mathematics (pardon my lack of "sharpness" on that, but, strictly speaking, we could go back to Aristotle), from its very logical foundations onward, is rooted on a fallacy. I wish to stress here that correcting that fallacy doesn't mean throwing to the bin all of the great accomplishments so far, it rather means we could enlarge our perspectives beyond what is today believed to be out of our reach.

As an anticipation, Walster talks about an "exception free system", which is a way to show that this "new" system (in the sense just given) must be simpler, not more complex than our current systems. This "new" system must still show some kind of instrinsic limit, though, and that is what I am (at a naive level) dis-expressing within the very last sentence in this document. However, let's finish the tour first.

>> Within Complexity, NP problems are said to be "intractable", and it is yet an open question whether or not P = NP.

Going back to Walster: "The use of interval methods provides computational proofs of existence and location of global optima. Computer software implementations use outwardly-rounded interval (cset) arithmetic to guarantee that even rounding errors and bounded in the computations. The results are mathematically rigorous." For example, the Kepler conjecture has been proved after 300 years by means of computers and outwardly-rounded cset arithmetic.

(6) We now can say: NP is too in the tractable domain, though NP is not P in that they represent the two opposite approaches to problem solving, the latter finding the correct solutions, the first discarding the incorrect ones.

Incidentally, if NP happened to be intractable, in real life we would forever be stuck in undecidedness, which is apparently not the case (and here I mean, apart from any heuristics: human beings don't need heuristics in every-day life, though every-day life is full of undecidable questions, rooted into the very structure of natural language).

>> Di Egidio asks what then is a "number" (or a "set") for the sake?

(7) We now can say (extensionally): a number (or a set) dis-is all we can do with-in and with-out it, i.e. the closed number system exhausts the whole domain of tractability, by tautological-within-self-referential foundation.

>> Golden shows[**] a family of number systems called "polysign numbers", having a natural number of signs.

(8) We now can say: Walster shows the "natural" closure of real numbers (avoiding undefined numbers and bounding computational errors); Golden shows the "natural" interplay between natural and real numbers (avoiding the asymmetries introduced with the imaginary numbers[***]); finally, Di Egidio shows (yet to be dis-proved), the general "natural" meaning of "number", as rooted into the concept of a subject which is the empty set (avoiding undefined reasoning).

>> Di Egidio screams, what's the outcomes then?

(9) We now can say: the outcome is the unified theory of all we can do with it (seriously).

>> Di Egidio cries, come on, you're saying "seriously"!?

(10) The outcomes are still to be inspected and worked out, but... even if only half of what is stated here has some reasonable foundation, then its incidence on everybody's lives could be dramatic, and to the better(!!). For instance, we have here the foundation for a final convergence of natural and logical languages, and, if you cannot imagine how that could only and only only change our lives for the better, then "You" fail.

If you managed to get to this point, I'll be looking forward to your knowledgeable dis-proofs.

(As you may guess, I do really need your feed-back.)

Thank you very much,

Julio

--------------------------
Julio Di Egidio
Analyst/Programmer
http://julio.diegidio.name

[*] More on Walster's Closed Sets in this thread (it's the sci.math group): http://mathforum.org/kb/message.jspa?messageID=6126425&tstart=0

[**] More on Golden's Polysigned Numbers on his web site: http://www.bandtechnology.com/PolySigned/index.html

[***] The asymmetries are not completely avoided, but I guess Mr Golden might not have heard of closed number systems, yet.

============================

Anthony A. Aiya-Oba
Prime Two Exclusiveness Conjecture
Posted: Mar 8, 2008 11:33 AM
http://mathforum.org/kb/message.jspa?messageID=6128731

Other than two, there exists no prime, whose sum of its factors equals prime. -Aiya-Oba (Poet/Philosopher).

Thus, P/1 + P/P = 3, is solely, and solely, P = 2.
Q E D

============================

Julio Di Egidio
Re: Prime Two Exclusiveness Conjecture
Posted: Mar 8, 2008 12:30 PM
http://mathforum.org/kb/message.jspa?messageID=6128733

2 dis-is Q E D

-LV

============================