[FOM] refs on feasible realisability
V.Sazonov at csc.liv.ac.uk
Wed Mar 29 19:54:12 EST 2006
Quoting Mirco Mannucci <mmannucc at cs.gmu.edu> Wed, 29 Mar 2006:
> I would like to know if anyone has heard of relevant research (and
> associated references) in the area of feasible realisability.
The term `feasible' can be understood at least in two ways: as
`polynomial-time computable' or as `physically realisable' (proper
feasibility). I am interested in both versions. But the latter is most
intriguing and has another reading as `ultrafinitism'. However, I am
not shure that everybody have the unique understanding of
ultrafinitism. It does not exist yet as a proper mathematical subject -
only various vague and may be divergent views.
> The reason why I am asking is that I am interested in the model theory of
> ultrafinitism, and, as it is well known, Kleene's realisability provides
> one of the main semantics for standard intuitionistic logic (in its last
> incarnation it became the effective topos, modest sets, etc.).
> Thus I wonder if somebody has tried to "restrict" realisability to a
> feasible subset of codes (or something along similar lines).
I am not sure that any traditional approaches, even via toposes, which
do not change crucially the logical foundations can approach to
*proper* feasibility. Surely, the ordinary intuitionistic logic behind
topoi is insufficiently radical for that, at least for that
understanding of feasibility which I assume.
Nevetheless, in the framework of the ordinary concept of PTime and the
ordinary intuitionistic logic some approaches to PTime realisability
are possible. I know one of S.Buss, another of S.Cook and A. Urquhart
(based on Dialectica Interpretation), and also my approach which is
just straightforward adaptation of Kleene realisability to a weak
intuitionistic theory of binary strings which is an analogue of so
called "Russian Constructivism" = HA + ECT + M. Recall that
HA is Heyting Arithmetic,
ECT is an extended formal version of Church Thesis,
M is the Markov's Principle.
I considered a weak theory T_0 of binary strings instead of HA.
The result is that the usual considerations of Kleene realisability
goes almost straightforwardly for the case of T_0 showing that some
"unary" restricted version of T_0 + ECT + M is constructive and also
showing that its full "binary" version is constructive iff P=NP.
Also it was shown that "constructive" for this theory means in a sense
"polynomial constructive". So, provability of
forall x exists y A(x,y) [A arbitrary formula with quantifiers]
implies provability of A(x,p(x)) for some PTime computable function p(x).
Note that with the presence of ECT this theory is essentially
intuitionistic (it is classically contradictory).
In particular, this theory does not prove totality of 2^n and that
provably recursive functions are exactly PTime computable ones. In this
sense it is a `feasible' theory (in the first version of feasibility
Corresponding realisability theory required to demonstrate that Turing
Machine computability is definable (even with the absence of total
exponentiation!), and, moreover, that Universal Turing Machine does
really exist and work as required. This was a bit subtle point and
required to define the concept of TM sufficiently carefully to
guarantee its correct behaviour in the "world" where the total
exponential function is absent.
This is published in
An equivalence between polynomial constructivity of
Markov's principle and the equality P=NP,
Siberian Advances in Mathematics, 1991, v.1, N4, pp. 92-121
(English translation of a paper in Russian published in
Matematicheskaja logika i algoritmicheskie problemy, Trudy Instituta
matematiki SO AN SSSR, 12, Novosibirsk, ``Nauka'', Sibirskoe
otdelenie, 1989, pp. 138--165.)
A hardcopy is available by request.
In the case of real (physical) feasibility, when not only exponential
function but even multiplication are partial functions, the situation
is completely different. Here not only Universal computable function
can hardly exist but also any kind of Church Thesis is doubtful to
hold. Let me recall my recent posting to FOM on formalising a toy
feasible arithmetic where 2^1000 is postulated as infinity
as well as my paper cited there, demonstrating how unusual should be
such a formalisation of `proper' feasibility. Note that all these
considerations on `proper' feasibility are mathematically quite
> Any input is appreciated
> All the best
> Mirco A. Mannucci
This message was sent using IMP, the Internet Messaging Program.
More information about the FOM