AIMXIUPDATES

Misc

• Room keys delivered at 14.00 at the Meeting room
• Internet connection
  • SSID CVS2010
  • PASS 324AIMXI24500
  • (WEP 128bit)
• Coffee at the left side of the Meeting room
• Excursion (27/3 Sat)
  • Meet at 9.00 at the bustop in font of the hotel entrance.
  • Destination: Himeji
  • Schedule: to be pasted.
  • Guide: Yatabe-san(mobile:XXXXX) and Matsuzaki-san
• Dinner (27/3 Sat)
  • The Sky buffet, 24th floor, Kobe Shoko Boeki Center Building.
  Hamabe-dori 5-1-14, Chuo-ku, Kobe, Phone: 078-252-7570
• In Sannomiya area of Kobe
  • Excursion participants are taken there by Yatabe-san/Matsuzaki-san
• Tea Ceremony (28/3 Sun)
  • Meet at 13.45 at the tea ceremony room on the 4th floor (the same floor as the Meeting room)
• Thorsten's Pictures

24/3 11.20 CodeSprint Discussion

Scheduling: Whenever the leader wants to start the sprint, the leader gathers the members...

• 1. Thorsten, Thomas, Bengt
  • PiSigma in Agda
  • Theory Sprint: Extensional equality
• 2. Catarina
  • Agsy
• 3. Nisse, Ulf, Catarina, Thorsten
  • Optimizing Agda
  • Structural equality
  • Together with 4., self-organizing
• 4. Nisse, Ulf, Andreas, Thorsten
  • Smarter productivity checker
  • Sized types in Agda (evidence based termination checking via sized types)
  • Theory Sprint: Modular nesting of inductive-coinductive types
  • Together with 3., self-organizing
• 5. Andreas, Makoto
  • Proof irrelevance and extraction
  • Whenever Andreas starts
• 6. Makoto, Bengt, Yoshiki
  • InformalArgumentInAgda
  • Using Agda to make informal arguments more convincing and easier to validate.
  • Start 25 14.00
• 7. Norio Kato
  • Specification of Agda-A (Java Agda)
• 8. Yoshiki, Matsuzaki, Bengt
  • Hoare Logic
• 9. Matsuzaki
  • Learning agda
• 10. Yatabe
  • Writing the paper on Specification processing system S3 using Agda.
• Discussion Sprint
  • Quotient types (Thomas)
  • Structural / Extensional equality (Thorsten)

To be further discussed in the afternoon.

26/3 Starting 9.30 (Coffee to be prepared around 9.00)

CodeSprint Discussion Records

• 1. Thorsten, Thomas, Bengt
  • PiSigma in Agda
  • Theory Sprint: Extensional equality
  • 25/3
  Not started properly yet, Started coding some fragments of Agda in PiSigma. Investigating PiSigma as Core Language, to which encode Agda. Discussion on ext. eq. and proof irrelevance: It's HARD.
  • 26/3
  See 1A.
  • 27/3
  Other things
  • 30/3
  Specified op sem, started specifying typing rules. Pi-Nano = PiSigma - Sigma -alpha = (Pi, Type : Type, Recursion)
  Want to have built-in Type soundness (evaluation during type checking is going to be shown never to fail)
  Agda impl of Pi-Nano
• 1A. Thorsten, Nisse, Ulf
  • Universe with infinite codes
  • 26/3 motivation : Univ of types with decidable equality. The files are in Agda repository.
    • With Agda codata: TypeConstructorsWhichPreserveGuardedness.agda
    • In PiSigma way in Agda TypeConstructorsWhichPreserveGuardedness.agda
  • 29/3 Cont. Universe of sets with decidable equality using codata.

     data Rec(A : infinity Set) : Set where
       fold : flat A -> A

     mutual
       -- A code can be infinite
       data Data : Set where  
         empty : Data
         maybe : infinity Data -> Data -- the only way to guard       
         sigma : usual

       -- El a does not contain infinite things, as you can see no infinity here
       El : Data -> Set
       El empty = bottom
       El (maybe A) = Rec(Sharp Maybe (El (flat A)))
       El (sigma A B) = the usual

     -- nat is the least fixpoint of Maybe
     nat : Data
     nat = maybe(Sharp nat)
     -- This is a shallow embedding of the recursive type definition

     z : El nat
     z = fold nothing

     s : El nat -> El nat
     s n = fold (just n)

   Trying to define eq for each El a.
   2 problems of Agda were fixed.
     1. Obviously the constructor Rec (any constructor) preserves guardedness,
        but Agda didn't know it.
        -> Nisse fixed it
     2. Agda thought this co-induction co-recursion is not strictly positive,
        because of the hidden argument A of flat.
        -> Fixed.

   reflexivity, substitubitiby, etc proven, but with termination problem.

• 30/3

  Yesterday's fix(making type constructors to be guardedness preserving)
  was too much of a fix : this also pass the type checking.
    data Endo A : Set where
      endo : (D -> D) -> D
    D = Rec(#(Endo D))

  New fix: type constructor only guards positive args.

  Now this made yesterday's Thorsten's example NOT pass.
  due to the matching occuring in the use of Sharp.

  Final fix: Let the positivity checker go inside the pattern when checking.   
  So now,
     flat : {A} -> inf A -> A
     flat (# x) = x
  passes positivity check as intended, and
     flat (# x) = x -> x
  woudln't.

  Other observation:
  Gurdedness preserving type constructor allows induction-recursion without
  induction. - A nice explanation of induction-recursion.
  (But needs strengthening the productivity checker.)

• 1C. Thorsten, Ulf
  • Reflection
  • 30/3
  Reflection = representing Agda values as Agda terms, as in RingSolver. Problem: user must manually write out the representation even thou

           you and Agda know what it represents.

Solution: Automaticaly getting the representation from the current goal.

     ...  
     open import NatSolver
     plus-zero : \all n -> n + 0 equiv n
     plus-zero = quoteGoal t in {! t !}-- t is the string rep of the goal type

     plus-zero = quoteGoal t in {! solve t !}

     plus-zero = quoteGoal t in solve t {! tt !}

     plus-zero = quoteGoal t in solve t _

  Currently the type of t is String and solve must parse t, but
  Thorsten is making it to be the Agda version of the whole of
  ISyntax.

    foo : String
    foo = quote (\ x -> x)

     ---> foo = "\x -> x"

  Need to keep/recognize higher level structure in normalised semantics?

  In future, we maybe able to use Agda as its own tactics language like Ltac.

• 2. Catarina
  • Agsy
  • 25/3
  Sent few reports to Frederik Working on some examples
  • 26/3
  Bigger examples. Normalization By Evaluation of Simply Typed Lambda example using Agsy.
  • 29/3
  The goal menu item "auto". Agsy now can do case splitting with the flag "-c". Looking at the AVL-tree library. Agsy can now prove:

    1+ : \all {m n} -> m ~ n -> 1 + m ~ 1 + n
    max~ : \all {i j} (bal : i ~ j) -> max bal ~ i

Trying also old Alf examples - good tests for inductive families.

    Symply Typed Lambda; Inductive-recursive def of Fresh list (context)
    Agsy can prove
      gtLemma : {Gamma Delta} ->
                (f : \all {n A} -> (n :: A in Delta) -> (n :: A in Gamma))->
                Gamma >= Delta

  Agsy can be used for finding counter examples with the flag "-d" (disprove).

• 30/3

  Nothing new.  Almost finished Normalization By Evaluation example.
  Sent few bug reports to Frederik.

• 3. Nisse, Ulf, Catarina, Thorsten
  • Optimizing Agda
  • Structural equality
  • Together with 4., self-organizing
  • 25/3
  Can typecheck Std Lib again with 2G, fixed memory leak Disc. on value representation "explicit substituion OR closure" "named variables vs deBruijn"
  • 26/3
  Yes. Making progress. One file (Nisse's example) type checkes with half the memory. Better handling of records (eta-expansion related). Conor's example.
  • 29/3
  Did an experiment on whether it's good to remove eta-expansion on records.

    Eta-eq on records with deep hiearchy are causing perf. prob. 
    Made sure don't eta-expands too much.
    Tried to remove eta-equality on records altoghter
    (When you want, you can still specify to use eta-expansion.)
    The result of experiment is that you do want eta-expansion most of times,
    because otherwise constraints solving (among projections on metas) doesn't work well.
    So we keep record eta-expansion, but try harder to avoid unnecessary expansion.

Figuring out why it's slow based on some examples.

• 30/3

  Decided it's not optimal to changing variable rep etc as a sprint. 
  More profiling on memory usage. -RTS flags. 

  Two things:
  1. Changing equality on Sharps
  2. Structural equality (after variable rep etc. are changed.)
     (There is a potential str.eq. would make Agda slow - so we may not
     do it after all.)(The necessity for str.eq. may be not so much.)

• 4. Nisse, Ulf, Andreas, Thorsten
  • Smarter productivity checker
  • Sized types in Agda (evidence based termination checking via sized types)
  • Theory Sprint: Modular nesting of inductive-coinductive types
  • Together with 3., self-organizing
  • 25/3
  Not yet.
  • 26/3 (Related to 3. too) Agreed on how to interprets data types and so on. Fixed the defect that the current termination checker is not modular w.r.t. extensional semantics. Discussed whether "notation with infinity and sharp are too low level" OR NOT. Will figure out what they mean and MAYBE later will give some sugar.
  • 29/3
  Some examples on use of sized types. Nisse's workaround, porting agda examples to mini-agda.
  Lots of discussions on productivity over the weekend. Found out how to interpret mutual inductive-coinductive types.

    mutual
     data D1 : Set where
       d1 : D2 -> D1
       d2 : inf D1 -> D1

     data D2 : Set where
       d3 : D1 -> D2
    (mu nu ? nu mu ?)
   ->
   should be combined into a family

     data D : Bool -> Set
       d1 : D true -> D false
       d2 : inf (D false) -> D false
       d3 : D false -> D true

• 30/3 See the 1B entry.
  • Andreas: Termination checking

  A patch submitted for new termination checking.

  The size differences recognized by Current Termination Checker are just
  {0, 1, infinity}.  New Termination Checker can count more than that.

  Consider the terminating

    f zero = zero  
    f (suc zero) = zero
    f (suc (suc n)) with zero
    ...                | m = f (suc n)

  which translates to

    f (suc (suc n)) = aux n zero
    aux n m = f (suc n)

  and confuses termination checker.

  A new flag "--termination-depth=2" (or 3,4,..) makes termination checker
  to see deeper.

  (Similar attenuation is done for whether termination checker
  uses dot-pattern arguments or not.)

  Caveat: On Tree-like data, it does not work so well.

• 5. Andreas, (X Makoto), Ulf, Nisse, Thorsten
  • Proof irrelevance and extraction
  • Whenever Andreas starts
  • 25/3
  Andreas' Talk on irrelevance. Realising problems with Metavariable and irrelevance
  • 26/3
  Andreas: Parametric polymorphism in Agda. Problem: With Mini-agda algorithm, Agad metavariable can be wrongly instantiated. Solution: Use Heterogeneous Equality. Before implementing, started Proving in Agda that the metatheory correct. Now trying to lift type equality proofs to translation functions. Plan: Will implement Hetrogeneous Equality in Mini-Agda and play around.
  • 29/3
  Heterogeneous eq on parametric function space. Letting TC to check irrelevance of an arg saves a lot of work for termination

    analysis (rather than using sized type)

([x : A] -> B = function type with irrelevant argument)

  Gamma |- t : [x : A] -> B  =  Gamma' |- t' : [x : A'] -> B'
  Gamma |- u : A                Gamma' |- u' : A'
  ---------------------------------------------------------
  Gamma |- t u : B[u/x]      =  Gamma' |- t' u' : B'[u'/x]

  A model is constructed in Agda (ParamSetoidModel.agda)
  mutual
    data TyCode : Set where
      U   : TyCode
      Pi  : (a : TyCode)->
            (f : el a -> TyCode) ->
            (F : {d' d : el a} -> eq d' d -> f d <= f d') -> TyCode
      Pi- : (a : TyCode)->
            (f : el a -> TyCode) ->
            (F : {d' d : el a} -> f d <= f d') -> TyCode

    el : TyCode -> Set
    el U = UCode
    el (Pi a f F) = Sigma ((d : el a) -> el (f d))
                          (\ g -> \all {d' d} (d'-d : eq d' d)->
                                       eq{f d}(g d){f d'}(g d'))
    el (Pi- a f F) = Sigma ((d : el a) -> el (f d))
                           (\ g -> \all {d' d} ->
                                       eq{f d}(g d){f d'}(g d'))

  Intuition for this hetero equality:
     "equal after erasing the irrelevant argument"

  300 lines.

  Conclusion : IT'S DONE.

• 30/3 Discussion continued. Implementing in Agda would be a major change. We are not clear about Syntax yet (Mini-Agda uses [..] but can't take them away from user.) Suggested for similarlity with dot-pattern

     (.x : A)...
     {.x : A}...

   The problem: We loose the invariant "when comparing two things they are
   of the same type."  This would necessiate extra check before instantiating
   meta variables.

   Cost/Benefit
      - extra check
      + parametric things doesn't have to be compared.

   Idea: Keep track of 'tainted' terms and
   do the extra checking only under parametric binders;  Then, we don't
   pay performance penalty so long as we don't use parametric functions.

• 6. Makoto, Bengt, Yoshiki
  • InformalArgumentInAgda
  • Using Agda to make informal arguments more convincing and easier to validate.
  • Start 25 14.00
  • 25/3
  See the page
  • 26/3
  See the page
  • 29,30/3
  See the page
• 7. Norio Kato
  • Specification of Agda-A (Java Agda)
  • 25/3
  Rearranging code for pattern matching so that the code gets closer to spec.
  • 26/3 Just continued....
  • 30/3 Inference rules in comments will be gathered later by Java-doc. Showing a sample inference rule:
    checkExpr : Expr -> ClosedType -> Term
    Sigma, Gamma |- infer e ===> e2 : t2 Sigma, Gamma |- hasType (e2 : t2) t ===> e3

  ---

  Sigma, Gamma |- checkExpr e : t ===> e3

   hasType : TypedTerm -> ClosedType -> Term

   try (Sigma, Gamma |- insertCast (e : t) t2) ===> yes e2

---

Sigma, Gamma |- hasType (e : t) t2 ===> e2

   try (Sigma, Gamma |- insertCast (e : t) t2) ===> blockedBy m
   ... ... 
  ---------------------------------------------------------
   Sigma, Gamma |- hasType (e : t) t2 ===> e2


   Java code is intended to look close to the rules.

• Discussion on the value of paper specification like Definition of SML. Th/U: Worthless, nobody reads, bound to contain errors, ... B: Much better than not having it, U: Writing the spec is useful, but
  N: ML ppl say The Def had an effect of ML implementor very cautious and

       stagnated new efforts on implementation.

• 8. Yoshiki, Matsuzaki, Bengt
  • Hoare Logic
  • 25/3
  Yoshiki gave to Bengt an overall explanation of what's done Cleaning up the code after 1mo break. Aiming to show the cleaned up code tomorrow.
  • 26/3
  Y. explained the cleaned up code to Bengt. Bengt saw Attach:TestHoare4.agda, suggested to M to make it an example code on Agda Wiki.
  Andreas: Better to have a standard "contributions" repository. Ulf: We already have as the "example" directory for Agad repository.

       "make test" would check whether any code is broken for the current Agda.

Three aspects:

  1. as Examples for learners.
  2. as Test suites.
  3. as Library

• 30/3

  Keishi Okamoto and Yoshiki discussed about the following:

• 31/3
  • A logic for small step semantics
    • By C P, we wish to express a property that “P holds during the whole execution of C”
    • In Dynamic Logic, one writes [ C ] P for “P holds just after the execution of C terminates (if it ever terminates),” but it does not say anything about what happens during the execution of C.
    • For instance, one wants to assert
      • sort an array a using an index i “i is in the range of indices of the array a”

• (*** C “interrupting process can assume some property P for C”

  • Encoding in Dynamic Logic
    • C P is encoded in Dynamic Logic ([C] P) as follows. Only the interpretation of equencers (;) differs from that in Dynamic Logic.
      • atomic P := [ atomic ] P
      • C1 ; C2 P := C1 P && [C1] C2 P
      • if B then C1 else C2 P := B => C1 P && NOT B => C2 P
      • while B do C P :=(B => C ; while B do C P) && (NOT B => P)
• 9. Matsuzaki
  • Learning agda
  • 25/3
  Asking Qs to Yoshiki -> Started to read on Bengt's book. Decided to learn by working on Hoare Logic.
  • 26/3 Continued reading Bengt's book, with Yoshiki's lecture materials.
  • 29,30/3 Practicing theorem proving in Agda, and reading Yoshiki's Hoare Logic code.
• 10. Yatabe
  • Writing the paper on Specification processing system S3 using Agda.
  • 25/3
  Started writing the paper Started on another problem: non-standard arithmetic in Agda

    with Thorsten's help ->
    Reading on Nisse's paper on beating productivity checker.

• 26/3 Continuing readin Nisse's paper.
• 29,30/3 Finished the 1st draft of the paper, continued reading Nisse's paper.

• Discussion Sprint
  • Quotient types (Thomas)
  • 25/3
    Integrated to Extensional equality topic.
  • 26/3 Implemented experimental equalty in PiSigma, to encode in PiSigma a high level equality that is equivalent to the Agda one.
  • Structural / Extensional equality (Thorsten)
  • 25/3, 26/3 Happened during/after Lunch -> see above.
• Discussion on Next AIM

Thorsten: (An announcement of DTP 2010, 9-10 / 6) Thorsten: AIM12

  In Nottingham.
  NSCSL? building

  Proposed date:

    8 Sep - 15 Sep?  (Conflict with Japanese meeting)
     ->
    1 Sep(Wed) - 7 Sep(Tue)? (Conflict with the beginning of chalmers new term?)

  Travel info will be put on wiki later.


  Excursion on Saturday.
     Bring a good pair of walking shoes and rain coats.
     From Ashford in the Water to Monzal Dale.