PhD position in proof theory at the University of Bath

[Alessio Guglielmi]

Dear Annatala,

I confirm Joe Shipman's interpretation: two algorithms might be different, according to some notion of equality to be specified, even if they compute the same function. Finding good notions of equality for proofs and algorithms is part of the problem that we are addressing in our research.

The issue is not what proofs and algorithms prove and compute but how they do so. For this, the representation of proofs and algorithms plays a key role. More precisely, it is not so much the language we use to represent proofs and algorithms that matters but our ability to break and recompose them so that we get useful normal forms. In other words, what matters is the composition mechanisms. By acting on them, we hope to find normal forms that are canonical representatives for good notions of equality.

Cheers,

-Alessio


> Begin forwarded message:
> 
> From: Annatala Wolf <a.lupine at gmail.com <mailto:a.lupine at gmail.com>>
> Subject: Re: PhD position in proof theory at the University of Bath
> Date: 3 March 2020 at 19:14:07 GMT
> To: Alessio Guglielmi <web.alessio.guglielmi at gmail.com <mailto:web.alessio.guglielmi at gmail.com>>
> Cc: Foundations of Mathematics List <fom at cs.nyu.edu <mailto:fom at cs.nyu.edu>>
> 
> On Tue, Mar 3, 2020 at 12:30 PM Alessio Guglielmi <web.alessio.guglielmi at gmail.com <mailto:web.alessio.guglielmi at gmail.com>> wrote:
> 
> Suffice to say that we are currently unable to decide whether two given proofs or two given algorithms are the same; this is an old problem that dates back to Hilbert.
> 
> Just a picky note which is probably obvious (and perhaps the above was intended as a joke), this problem is not just "currently" inaccessible to us. The general problem is NRNC (both it and its complement are undecidable), which is easy to show: assume a program exists that tells you if two algorithms are the same, then pass it 1) an algorithm that outputs true iff some undecidable process terminates (there must be some algorithm for which this is true even if we don't know which), and 2) an algorithm that always outputs true. This contradicts the undecidability of an undecidable algorithm, which means the assumption must be false. The same idea works for the complement.
> 
> -- 
> /* Annatala Wolf, Lecturer
>  * Department of Computer Science and Engineering
>  * The Ohio State University
>  */
> enum E{A;System s;String t="/* Annatala Wolf, Lecturer%n * Department of Computer Science and Engineering%n * The Ohio State University%n */%nenum E{A;System s;String t=%c%s%1$c;{s.out.printf(t,34,t);s.exit(0);}}";{s.out.printf(t,34,t);s.exit(0);}}


> Begin forwarded message:
> 
> From: Joe Shipman <joeshipman at aol.com <mailto:joeshipman at aol.com>>
> Subject: Re: PhD position in proof theory at the University of Bath
> Date: 4 March 2020 at 00:52:49 GMT
> To: Annatala Wolf <a.lupine at gmail.com <mailto:a.lupine at gmail.com>>
> Cc: Alessio Guglielmi <web.alessio.guglielmi at gmail.com <mailto:web.alessio.guglielmi at gmail.com>>, Foundations of Mathematics List <fom at cs.nyu.edu <mailto:fom at cs.nyu.edu>>
> 
> I don’t think the notion of algorithms “being the same” that was intended was “calculates the same function”. It is clear that one can have essentially different algorithms calculating the same function, where the proof that they calculate the same function may be much more complicated than the algorithms themselves.
> 
> Whether two proofs are “the same“ maybe a bit harder to address satisfactorily, because the inter-translatability of different formalisms for algorithms is better developed than for proofs. However, reverse mathematics provides one way to address this. Conway and I suggested another in our paper “Extreme Proofs”, in which we distinguished between seven different proofs of the irrationality of the square root of 2 by a “scope test”: each proof had a different domain of generalizability (which other irrational numbers the proof could be applied to).
> 
> — JS
> 
> Sent from my iPhone
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200304/1a27b7ec/attachment-0001.html>