[FOM] refs on feasible realisability

[Vladimir Sazonov]

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 
mentioned above).

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 
http://www.cs.nyu.edu/pipermail/fom/2006-February/009746.html,
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 
rigorous.


Best wishes,

Vladimir Sazonov


>
> Any input is appreciated
>
> All the best
>
> Mirco A. Mannucci


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.