Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Partial functions and their inversion in Coq.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Partial functions and their inversion in Coq.


chronological Thread 
  • From: jean-francois.monin AT imag.fr
  • To: "Koprowski, A." <A.Koprowski AT tue.nl>
  • Cc: <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Partial functions and their inversion in Coq.
  • Date: Tue, 8 Nov 2005 17:31:41 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello Adam,

Koprowski, A. a ecrit :
 > 
 >   Dear all,
 > 
 >  During my work I encountered the following problem, to which I think I
 > found a solution just I'd like to confirm that my line of reasoning is
 > correct and that there is no simpler approach.
 > 
 >  I need to specify a partial, injective function on natural numbers
 > (mapping on natural numbers) and I need to be able to compute its
 > inversion. I _definitely_ don't want to use classical logic so I suppose
 > in general my task is hopeless as even if I know that the inverse exists
 > (function is injective) I may not be able to compute it efficiently. Is
 > that true?

You may not even be able to compute the inverse at all, if the domain
is infinite and if you have no computable bound on the source, given 
the target.


 > 
 >  However in my problem the domain of mapping is always finite which
 > should make the task feasible. The approach I was thinking of is to
 > define the function as a relation with appropriate constraints and with
 > the number indicating the maximal natural number that belongs to the
 > domain or range of the function. In Coq it would be something like:
 > 
 > Record natFun : Type := {
 >   nf:      relation nat;
 >   lok:     forall i j j', nf i j -> nf i j' -> j = j';
 >   rok:     forall i i' j, nf i j -> nf i' j -> i = i';
 >   size:    nat;
 >   size_ok: forall i j, nf i j -> i <= size /\ j <= size
 > } 
 > 
 >   To compute inverse of the function I simply take the transposition of
 > the relation. To compute f(i) I look at nf(i, j) for all j <= size. If
 > none holds 'i' is not in the domain of the function. If I find nf(i, j)
 > to hold for some 'j' then f(i) = j and because of 'lok' I know that this
 > 'j' is unique. Does it make sense?

Yes

 > Is there a simpler approach that Ican take?

No, unless you have further information on nf.
E.g. if nf known to be increasing, you may attempt to reduce 
the computation time of its inverse using dichotomy.
Conversely, successfully computing the inverse without needing
to try all possibilities amounts to saying that you have some
piece of information on nf in your hands.

Hope this helps,

  JF

 >  
 >   Thanks a lot in advance!
 >   Kind regards,
 >    Adam Koprowski
 > 
 > --
 > ========================================================================
 >  Adam Koprowski, 
 > (A.Koprowski AT tue.nl,
 >  http://www.win.tue.nl/~akoprows)
 >  Department of Mathematics and Computer Science
 >  Eindhoven University of Technology (TU/e)
 >  The difference between impossible and possible lies in determination
 >       Tommy Lasorda 
 > ========================================================================

-- 
Jean-François Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 03 72
F-38610 GIERES                fax (+33 | 0) 4 56 52 03 44 





Archive powered by MhonArc 2.6.16.

Top of Page