Equality of functional values
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20070130 (13:55) 
From:  skaller <skaller@u...> 
Subject:  Re: [Camllist] Equality of functional values 
On Tue, 20070130 at 14:24 +0100, Andrej Bauer wrote: > Simon Frost wrote: > > I'm trying to use a software package written in ocaml (IBAL), however, > > it fails a test due to 'Fatal error: exception Invalid_argument("equal: > > functional value"). It seems that equality isn't defined for functional > > values in OCAML (although I'm not an expert), so I'm wondering what the > > workaround is. > > This may not sound very helpful, but: you are doing something wrong if > you need to rely on equality of functions. Equality of functions is not > computable. > > A suitable workaround would be to tell us what it is that you are doing, > and we will tell you what to use instead of functions (if possible). To > give you an idea of what you I am talking about: > > Suppose you came to us and complained that you cannot compare > polynomials with integer coefficients, and it turned out that you > represent polynomials as functions. We would then tell you not to do > that, and represent polynomials as arrays (or lists) of coefficients, or > objects, or some other data structure that is equipped with decidable > equality. Actually the idea 'equality of functions is not computable' is misleading .. IMHO. Equality of programmer written 'functions' should always be computable: more precisely one hopes every function could have a mechanically verifiable proof of correctness and wished programming languages provided an easy way to prove one. Of course for an arbitrary function, equality isn't decidable, but programmers don't write arbitrary functions (except in error). Andrej's suggestion amounts to a proof technique: use some fixed function (which is equal to itself) plus a comparable data structure. This may not be so easy to do though. BTW: Felix is one of the few general languages around that actually allows a statement of semantics: typeclass SemiGroup[t with Eq[t]] { virtual fun add: t * t > t; axiom assoc(x:t, y:t, z:t): add(x, add(y,z)) == add(add(x,y),z); } These axioms are checkable: instance SemiGroup[int] { fun add:int * int > int = "$1+$2"; } axiom_check(1,2,3); however there's currently no way to state and prove theorems. It would be interesting if someone had some idea how to use one of the existing theorem provers to act as a proof assistant (verify user given proof, filling in enough 'gaps' in the formal steps to make it practical). An extension to Ocaml which allowed for semantics might be interesting: the usual technique is to just put comments: that's pretty weak in this day an age isn't it?  John Skaller <skaller at users dot sf dot net> Felix, successor to C++: http://felix.sf.net