Re: New PAKCS release (Version 1.8.0)

From: Sebastian Hanowski <seha_at_informatik.uni-kiel.de>
Date: Thu, 05 Apr 2007 10:46:49 +0200

* Am 04.04.07 schrieb Bernd Brassel:
>
> On Wed, 4 Apr 2007, seha_at_informatik.uni-kiel.de wrote:
>
> > I'd like to point out that addition only requires that argument to
> > be ground on which the recursion takes place. Such equations then
> > become either solvable or refutable with partial evalutation and
> > first-order unification only. Narrowing should not be needed. Must
> > have to do with
>
> Yes, this would be a possible way to formalize addition by a unary
> representation of numbers. For an actual implementation view however,

Sorry to Wolfgang, seems I was a little of topic. Moreover, 'partial
evaluation' possibly is the wrong term here, because having a try with
this in Curry revealed that the usual evaluation behaviour is enough.
Given
        data Nat = Zero | Suc Nat

and addition defined with respect to the first argument

        plus :: Nat -> Nat -> Nat
        plus m n = case m of
                    Zero -> n
                    (Suc m) -> Suc (plus m n)
then
        plus m n

for any instantiated m will reduce to an m-deep constructor prefix for
arbitrary n. Such that for any x an equation

        plus m n =:= x

will trivially be either solvable or refutable.
Whereas one can define multiplication

        times :: Nat -> Nat -> Nat
        times m n = case m of
                    Zero -> Zero
                    (Suc m) -> plus (times m n) n

such that equations

        times Zero n =:= x
and
        times (Suc Zero) n =:= x

will trivially be either solvable or refutable for arbitray n and x this
doesn't hold for

       times m n =:= x

with 2 <= m any more since the second argument will be distributed to
both argument positions of addition.

Concerining partial evaluation I have no clue how far one can this in
Curry. But perhaps it doesn't always have to be type-checking to
statically refute programs violating invariants on /values/. For example
given

        minus :: Nat -> Nat -> Nat
        minus m n | m =:= plus n x = x where x free

maybe a compiler performing partial evaluation could warn that a program

        bang = minus (Suc Zero) (Suc (Suc Zero))

isn't well defined, because the constraint Zero =:= Suc _ is already
known to fail at compile time.


Best regards,
Sebastian

_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Apr 11 2007 - 11:57:07 CEST

This archive was generated by hypermail 2.3.0 : Do Feb 01 2024 - 07:15:07 CET