# 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.

- 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

- 26/3

- 27/3

- 30/3

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 : Ā → 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

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

- 26/3

- 29/3

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

- 26/3

- 29/3

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

- 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

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

- 30/3
See the 1B entry.

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

- 26/3

- 29/3

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

- 26/3

- 29,30/3

- 7. Norio Kato
- Specification of Agda-A (Java Agda)
- 25/3

- 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

- 26/3

“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”

- A logic for small step semantics

- 31/3

- (*** 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)

- C P is encoded in Dynamic Logic ([C] P) as follows. Only the interpretation of equencers (;) differs from that in Dynamic Logic.

- Encoding in Dynamic Logic

- 9. Matsuzaki
- Learning agda
- 25/3

- 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

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.