Re: Intended meaning

From: <kahl_at_cas.mcmaster.ca>
Date: Thu, 25 Oct 2007 13:58:12 +0000

Sergio Antoy wrote:
>
> Given the following program:
>
> test = 1+x ? zero x where x free
> zero 0 = 0
>
> what should the evaluation of test produce?

Taking the liberty to replace (1+) with (Succ :: Nat -> Nat),
the system I presented at WFLP this summer produces the equivalent of

  Succ (x where x free) ? 0

A one-page PDF of the deduction is available at:

http://sqrl.mcmaster.ca/~kahl/PMCFLP_Antoy_Succ.pdf

(I am afraid the previous attachment had a problem --- sorry!)


Wolfram
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Thu Oct 25 2007 - 17:47:31 CEST

This archive was generated by hypermail 2.3.0 : Thu Sep 19 2019 - 07:15:07 CEST