coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Partial functions and their inversion in Coq., Koprowski, A.
- Re: [Coq-Club] Partial functions and their inversion in Coq., jean-francois . monin
Archive powered by MhonArc 2.6.16.