[Agda] Bin._<_
Serge D. Mechveliani
mechvel at botik.ru
Sat Aug 4 13:34:53 CEST 2012
On Fri, Aug 03, 2012 at 01:37:34PM -0400, James Deikun wrote:
> On Thu, 2012-08-02 at 17:04 +0400, Serge D. Mechveliani wrote:
> > People,
> > I have a beginner question. Probably, it is on usage of lib-0.6.
> >
> > Please, what stands for "<" for Bin (binary naturals) ?
> > I need to test a binary variant for `length' and `lookup':
>
> You really have about 5 options here:
>
> 1) Use qualified prefix syntax:
>
> open import Data.Nat
> open import Data.Bin as Bin
>
> [later ...] Bin._<_ a b
>
> [..]
So, I try it to compare two binary naturals obtained by applying
fromBits:
----------------------------------------------------------------
module Lookup where
open import Data.Bool
open import Data.String
open import Data.Digit
open import Data.List
open import Data.Nat
open import Data.Bin as Bin
open import Foreign.Haskell
open import IO.Primitive
open import Prelude hiding (IO; putStrLn)
l : Bin
l = fromBits (0b :: 1b :: [])
n : Bin
n = fromBits (0b :: 1b :: 1b :: [])
b : Set -- ? what must be is its type?
b = Bin._<_ n l
main : IO Unit
main = putStrLn (toCostring (show b))
-----------------------------------------------------------
1. What does this mean `[later ..]' in
> [later ...] Bin._<_ a b
?
2. Data.Bin of lib-0.6 declares
--------------------
infix 4 _<_
-- Order relation. Wrapped so that the parameters can be inferred.
data _<_ (b1 b2 : Bin) : Set where
less : (lt : (Nat._<_ on toNat) b1 b2) -> b1 < b2
--------------------
(I replaced math symbols).
2.1. I am looking into the reference manual page of
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Keywords
and do not find the keyword `on'. What does `on' mean?
Does it mean here that less b1 b2 is evaluated via conversion to
unary Natural, as
(toNat b1) < (toNat b2) ?
If so, then I do not need it, because I intended a fast comparison, and
toNat has an exponential cost.
2.2. Apart from the computation cost, what to set in my program instead
of b = Bin._<_ n l in order to obtain a Boolean value for
comparison of these two binaries?
2.3. It is difficult for a newbie to understand these things.
Can people comment the meaning of the declaration
data _<_ (b1 b2 : Bin) : Set where
less : (lt : (Nat._<_ on toNat) b1 b2) -> b1 < b2
in Data.Bin in lib-0.6 ?
What may be examples of its usage a) in ordinary computation,
b) may be, in a proof
?
Does it imply that _<_ : Bin -> Bin -> Set,
that _<_ takes two binaries and returns a small abstract type with
operation `less' ?
Probably, the returnd type is non-empty iff (toNat b1) < (toNat b2)
-- ?
What is the type of the argument of `less' ?
What does it denote the last occurence of `<' (in `b1 < b2'),
is it the one from `data _<_' ?
3. I hope one can program fast ordering comparison on Bin
(linear cost in the bit list length) by applying toDigits and by
comparing the bit lists. But maybe lib-0.6 already has something for this?
A bit of philosophy:
generally, I have an impression that Agda cares more for proofs than
for an ordinary computation support. Providing proofs via types is
interesting, all right (needs investigation).
I and some other people need a language (and compiler) which _also_
gives possibility to formulate efficient algorithms for a real-world
mathematics. Something like this: Haskell + GHC + dependent types.
For example, having an algorithm of O(n^3), it is not appropriate to
replace it with a program of O(2^n), neither even of O(n^4), despite
even possible proof simplification for various algorithm properties.
The reason is evident.
Also the very algorithm formulation must be as simple as possible, for
readability. To what extent a program can be complicated in order to
accomodize it for proofs -- this may be a question.
Also I expect that on the real _today_ practice, 99% of proofs would
appear by an human thinking and typing the hints to the system. Still
this may be useful, due to the possibility of automatically checked
certificates. Because a human often gives an erroneous proof, and such
are stopped by the proof assistant.
Thank you in advance for explanation,
------
Sergei
More information about the Agda
mailing list