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

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".

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].

(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

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

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.

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.