- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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

Date: Thu, 05 Apr 2007 10:46:49 +0200

* Am 04.04.07 schrieb Bernd Brassel:

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
: Mi Jan 22 2020 - 07:15:06 CET
*