_at_ Wolfang Lux
>
> I would (also?) like to see Curry implementations to solve equations
> like
> x + 1 =:= 4
> by binding x to 3. However, if they do not at present, this is not the
> fault of (=:=) but of (+) which requires ground arguments. And in fact
> if Curry implementations in the future will solve that equation, I hope
> that they will not do it by narrowing, but by using the algebraic laws
> of integer arithmetic (i.e., using a constraint solver).
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
Presburger arithmetic, the additive fragment of arithmetic, beeing
decidable.
One can exploit this in type theory for having the subtraction of the
naturals beeing only type correct if the second argument is smaller than
the first with the type-checker deciding wether the first is a sum
involving the second.
-------------------------------------------------------------
( n : Nat !
data (---------! where (---------! ; !------------!
! Nat : * ) ! O : Nat ) ! |+ n : Nat )
-------------------------------------------------------------
( m, n : Nat !
let !----------------!
! plus m n : Nat )
plus m n <= rec m
{ plus m n <= case m
{ plus O n => n
plus (|+ m) n => |+ (plus m n)
}
}
-------------------------------------------------------------
( m, n : Nat ; p : m = plus n x !
let !--------------------------------!
! minus m n p : Nat )
minus m n p <= case p
{ minus (plus n m) n refl => m
}
-------------------------------------------------------------
inspect minus (|+ (|+ (|+ O))) (|+ (|+ O)) refl => |+ O : Nat
-------------------------------------------------------------
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:06 CEST