|
|
Jack Campin - bogus address wrote:
> [complicated mess of quotation-within-quotation, but this seems to be
> Manna and Waldinger]
>
> > Unless we have a philosophical commitment to intuitionism, maintaining
> > constructiveness when it is not required can only make a proof system
> > more cumbersome to use. We have seen that certain programs cannot be
> > derived from their specifications in a constructive logic, but can be
> > derived in a classical logic upon which minimal restrictions have been
> > imposed ... ': Zohar Manna and Richard Waldinger, 'Constructive Logic
> > considered Obstructive' (typescript, n.d.), 8.
>
> There is a trick that comes out of the theorem-proving-on-top-of-Scheme
> community that draws a completely different moral. You can extend the
> Curry-Howard isomorphism to interpret classical logic; Peirce's law
> ends up being the type of call-with-current-continuation. But this
> isn't restricting classical logic, it's reinterpreting it.
But does it allow you to perform Program Synthesis?
BTW Would you say that proofs correspond to programs or to program
executions? And what does Curry-Howard say?
C-B
> ============== j-c ====== @ ====== purr . demon . co . uk ==============
> Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760
> <http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975
> stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557
|
|