* 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