- HTML version, org-mode source
____________________
RECORD OF AIM XVII
____________________
Table of Contents
_________________
1 Participants:
2 (7 May Tue)
.. 2.1 Supper 18:30 ~
3 8 May Wed.
.. 3.1 Agenda discussion, orientation : 9.00 - 10.00
.. 3.2 James Chapman(+all): On copatterns : 10.30 - 11.45, 14.00 - 17.30
4 9 May Thr.
.. 4.1 Yoshiki Kinoshita: Category Theoretic Structure of Setoids (with John Power)
.. 4.2 James Chapman: On copatterns: 11.00 - 12.00
.. 4.3 (James Chapman and Makoto Takeyama only): (Not) speeding up Agda type checking : 13.30 - 14.00
.. 4.4 Shuji Kinoshita: On Granström's World : 14.00 - 15.30
.. 4.5 X-Sprint : 15.45 - 18.00
5 10 May Fri. : Excursion
6 11 May Sat.
.. 6.1 James Chapman : Formalizing restriction categories : 09.00 - 10.40
.. 6.2 Bengt Nordström : Incremental Type Checking : 11.20 - 12.00, 14.00 - 15.40
.. 6.3 MT : Meta-verification and validation 16.00 - 17.00
.. 6.4 X-Sprint : 17.00 - 18.00
7 12 May Sun.
.. 7.1 Liyang Hu : Software Transactional Memory : 09.00 - 11.40
.. 7.2 X-Sprint : All : 14.00 - 17.30
.. 7.3 Wrap up
.. 7.4 JC and MT:
.. 7.5 YK and JC:
.. 7.6 SK
.. 7.7 JC and SK and MT
8 13 May Mon.
.. 8.1 X-Sprint, Wrap-up
.. 8.2 Next AIM Discussion:
1 Participants:
===============
- James Chapman (Institute of Cybernetics)
- Shuji Kinoshita (NAIST)
- Yoshiki Kinoshita (Kanagawa U)
- Bengt Nordström (Chalmers)
- Makoto Takeyama (Kanagawa U)
- Liyang Hu (Tsuru Capital LLC / U Nottingham)
2 (7 May Tue)
=============
2.1 Supper 18:30 ~
~~~~~~~~~~~~~~~~~~
3 8 May Wed.
============
3.1 Agenda discussion, orientation : 9.00 - 10.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
§ 3.1.1 Planned schedule: [http://wiki.portal.chalmers.se/agda/uploads/Main.AIMXVII/AIMXVIITImeTalbe.pdf]
(Excursion moved to Friday due to the forcasted rain on Saturday.)
§ 3.1.2 Actual
---------------------------------------------------------------------------------------------
Wed JC 10.30 - 11.45 On Copatterns
JC, All 14.00 - 17.30 Continued to discussion sprint? on copatterns
---------------------------------------------------------------------------------------------
Thr YK 09.00 - 10.40 Category Theoretic Structure of Setoids
JC 11.00 - 12.00 On Copatterns (cont.)
(JC,MT) 13.30 - 14.00 ((Not) speeding up Agda type checking)
SK 14.00 - 15.30 On Granström's Worlds
All 15.45 - 18.00 X-Sprint
15.45 - 17.50 - JC,MT,BN : Discussion on Copatterns (cont.)
- BN: Explanation of batch type checking
- SK: Agda formalisation of the category of Granström's worlds
---------------------------------------------------------------------------------------------
Fri Excursion
---------------------------------------------------------------------------------------------
Sat JC 09.00 - 11:00 Formalizing restriction categories
BN 11.20 - 12:00 Incremental Type checking
BN 14.00 - 15.40 Incremental Type checking (Cont.)
MT 16.00 - 17.00 Meta-verifcation and validation
All 17.00 - 18.00 X-Sprint
---------------------------------------------------------------------------------------------
Sun LH 09.00 - 11.30 Software Transactional Memory
All 14.00 - 17.00 X-Sprint
Mon All 09.00 - 12.00 X-Sprint, wrap-up.
---------------------------------------------------------------------------------------------
3.2 James Chapman(+all): On copatterns : 10.30 - 11.45, 14.00 - 17.30
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
§ 3.2.1 Summary
JC led the discussion on coinduction and copatterns based on
,----
| Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer.
| Copatterns - Programming Infinite Structures by Observations -. POPL 2013
| http://www.tcs.ifi.lmu.de/~abel/popl13.pdf
`----
up to Section 5.1
- BN: Analysing general scheme of coinductive definition with nested
(co)patterns are too complex. We should study simple copatterns /
corecursors like we do for inductive types.
- Lots of discussions on the sense of "values" and "getting stuck"
- Extension to dependent types where type equality involves
computation seems non trivial.
§ 3.2.2 More details
- BN: If we take "observers define a coinductive type" seriously, a
suitable notation for declaring typing of observers is something
like
,----
| Stream A = { X : Type ; head : X → A ; tail : X → X }
`----
not like field label declarations
,----
| Stream A = { head : A ; tail : Stream A}
`----
- BN: It is hard to try reasoning about the general definition schema
with nested (co)patterns as in the paper. *We could study what
corresponds to the recursor / elimination principle for coinductive
types and explain general definitions in terms of that.* (Like the
pattern matching definition of `_+_' is understood in terms of the
recursor on ℕ.)
- The sense of "values" (which affects the sense of "not getting
stuck", "progress" and "coverage")
- To say any expression of a negative type is a value seems rough.
Is the expression "f ∘ g" a value? (function types are negative.)
- What the values of a coinductive type are is not explained as
clearly as those of an inductive type.
- Is there a problem with the usual "a stream value is one that
has cons-headed form with head and tail revealed"? Or is a
stream value anything that we know for sure we can make into a
cons? (Is the latter just turning the theorem "don't go wrong"
to a definition?)
- Is it inappropriate to ask what they are?
- Values usually are considered for the purpose of conversion
checking (besides for being answers). But the paper's type system
does not require conversion checking, so the role of value-ness in
that regard is unclear.
- The sense of polarity of types? Positive = defined by introduction,
Negative = defined by elimination?
- Relationship between the polarity of types and the bidirectional
checking? Here checking vs inferring more or less align with
polarity of the type (positive → checked against (at first);
negative → inferred). Is there some significance to this? How does
this relate to the usual alignment with the form of the term
(introductory → checked against a type; neutral → inferred)?
- Why the main function must have positive type? Not all objects of
negative type seem infinite or unprintable.
- What is the status of the reduction relation generated from the
observation rules of a program in Sec 4? Is this the operational
semantics of the program? Non-deterministic without a strategy?
(while evaluation contexts usually are considered in order to
specify a strategy?)
- It seems non-trivial extend all this to dependent types where type
conversion checking involves computation, particularly Lemma 7.
- Missing lemma to apply Lemma 8 for Theorem 4?
- "If Γ ⊢ E[f] : B then Γ | Σ(f) ⊢ E : B"
Ok by induction on E.
- BN: Starting with general copatterns makes it hard to see what is
happening. What it means to be an object of a coinductive type
should be defined to be being able to prove that the (simple)
observations on that objet is defined. Type system should guarantee
that complex observations are defined.
- The sense of values and getting stuck again.
- Is the seemingly non-deterministic reduction relation in Sec 4 CR?
- Is the sense of "getting stuck" dependent on reduction strategies?
- Usually a programming langauge semantics comes with a
deterministic strategy and no questions arise about CR or
various senses of getting stuck. The paper is more in the lambda
calculus tradition?
- Finished for today at the end of Sec 5.1
4 9 May Thr.
============
4.1 Yoshiki Kinoshita: Category Theoretic Structure of Setoids (with John Power)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Discussed the paper
,----
| Power, J. and Kinoshita, Y.
| Category theoretic structure of setoids.
| Theoretical Computer Science. ISSN 0304-3975 (In Press)
| http://opus.bath.ac.uk/34231/1/main.pdf
`----
- Mathematical formulation of a setoid where the equivalence relation
is replaced by family of sets with refl, sym and trans witnessed by
families of functions without coherence requirements.
- Discussion on the sense of formalising naive set theory based
mathematics in Agda.
- Structures on the category Equiv of equivalence relations (complete,
cocomplete, exponentials) and Setoid of setoids (products,
coproducts, exponentials, no equalisers and coequalisers).
- Equiv-enriched Seotid and its weak eqaulisers (inserters).
- Discussion on the senses of the terms "proof irrelevance"
1. Identifying all proofs (1a. of certain propositions, or 1b. that
appear as function arguments at positions that are declared
irrelevant.)
- justified by not analysing proofs / not using proofs relevantly
in computation.
2. Never comparing two proofs (while not positively identifying the
two).
3. Only caring about existence / non-existence of proofs
- 1. is the usual technical meaning, but how to call 2? How does 3
relate with 1 and 2 exactly?
4.2 James Chapman: On copatterns: 11.00 - 12.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Continued the discussion from Wednesday.
- Still trying to understand the sense of "not getting stuck" from the
definition of copattern coverage.
- Why don't we see "getting stuck on a variable"? What is preventing
computation under context in this system?
4.3 (James Chapman and Makoto Takeyama only): (Not) speeding up Agda type checking : 13.30 - 14.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Experimented on how to speed up type checking / lessen memory usage on
JC's category theory code.
- Use of "abstract" helped slightly but there were not much
opportunity for it for the code already heavily annotated for
irrelevance.
- Moving let definitions to where clause helped one file but made
things worse for the overall build.
- Splitting files up
4.4 Shuji Kinoshita: On Granström's Wold : 14.00 - 15.30
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Discussed the paper
,----
| Johan G. Granström. A new paradigm for component-based development.
| JOURNAL OF SOFTWARE, VOL. 7, NO. 5, MAY 2012
| https://www.academypublisher.com/~academz3/ojs/index.php/jsw/article/view/jsw070511361148
`----
- Worlds, world maps, the category of world
- Things that were figured out during discussion, which turned out to
be written in the later part of the paper:
- For w = (C, R), w ⇒ X is like the W-type W(C,R), but parameterised
in the type X of leaves. W(C,R) ≅ w ⇒ 1.
- w ⇒ X is the free monad on the functor ⟦ w ⟧ X = Σ c : C . R c → X
- a world map w₁ ⊸ w₂ is a container map w₂ → w₁̂̂*
- The equality on programs seems a usual inductive predicate - why is
it called a new primitiv of type theory?
- It was not clear what exactly is new compared with the original
Hancock-Setzer or with container works.
4.5 X-Sprint : 15.45 - 18.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
§ 4.5.1 JC and MT, BN
Continued copatterns discussion.
- In the statement of case 4 of Lemma 14, ⊬v e : B should be read ⊢ e
: B and ⊬v e : B for the proof of Thm 15 (Progress)?
- In the proof of Progress, why is E₁, and not E₂, shown to be a value
context?
- From the statement of Progress, "not getting stuck" is seen to apply
only for closed terms.
- To say any expresssion of a negative type is a value still felt
unsatisfactory as an explanation of what a value of a coinductive
types is.
- Looked for an answer for the above in Granström's thesis, which
turned into a wild goose chase. Found no Easter eggs.
§ 4.5.2 BN
Worked on the explanation of batch type-checking.
§ 4.5.3 SK
Worked on Agda formalisation of Granström's worlds.
5 10 May Fri. : Excursion
=========================
- 09.11 - 10.24 : From Shonan OVA to Enoshima Station
[http://goo.gl/maps/vUe0Y]
- 10.24 - 15.40 : Walk along Sagami Bay beach
[http://goo.gl/maps/aDwyo]
- 12.40 - 14.40 : Lunch: Shabu Shabu 'Viking' buffet
- 16.10 - 16.40 : To Inamuragasaki Onsen [http://goo.gl/maps/YXtlZ]
- 16.40 - 19.00 : Bath
[http://inamuragasaki-onsen.com/ofuro/index.html]
- 19.00 - 20.40 : Dinner [http://www.main-inamuragasaki.jp/index.html]
- 20.40 - 21.10 : To Shonan OVA
6 11 May Sat.
=============
6.1 James Chapman : Formalizing restriction categories : 09.00 - 10.40
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Discussed the paper
,----
| James Chapman, Tarmo Uustalu and Niccolò Veltri.
| Formalizing restriction categories. PCC 2013
| slides url?
`----
§ 6.1.1 Formalising frameworks of Cockett and Lacks "Restriction Categories"
- Partial map categories
- Restriction categories
§ 6.1.2 Categoraical Approaches to Partiality
- Partial map categories. Partial map synthed from toal maps
- Partial product categories (di Paola, Heller; Robinson, Rosolini),
Restriction categories (Cockett, Lack) - axiomatic approaches
- Partila map classification - sometimes pmaps are the Kleisili maps
of a monad on the toal map category
- Recusion categories (di Paorla, Heller). Turing categories (Cockett,
HExtra) - computational.
§ 6.1.3 Restriction Categories
- For f : A → B, has f̅ : A → A, which
- R1 : f ∘ f̅ = f
- R2 : f̅ ∘ g̅ = g̅ ∘ f̅
- R3 : g̅ ∘ f̅ = rest(g ∘ f̅)
- R4 : ...
- <Looking at Agda code> type in types. Het equality. With many axioms
for extensionality and quotienting.
§ 6.1.4 Restriction Categories: Examples
§ 6.1.5 Stable Systems of Monics
§ 6.1.6 Partial Map Categories
§ 6.1.7 Partial Map Categories : Examples
§ 6.1.8 From Partial Map Categories to Restriction category
§ 6.1.9 From Restriction category to Partial map cat
- Needs idempotent splitting.
- X ≅ Par(Total(X), M)
§ 6.1.10 Wrap-up
- Check up the notion of stable factorization system
- Check up those old papers from late 80's referred in Robin's paper,
like those of Giuseppe Rossolini.
- Also the relationship between Set and Rel as detailed in Peter
Johnstone's book.
6.2 Bengt Nordström : Incremental Type Checking : 11.20 - 12.00, 14.00 - 15.40
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
§ 6.2.1 Syntax
,----
| a ::= i | (a e) -- application, avoiding beta-redex
| e ::= a | Set | Π e f | fun f
| f ::= lam x e
`----
§ 6.2.2 Declarations
,----
| c₁ : t₁ ; ... ; cn / tn
`----
§ 6.2.3 Steps
1. No defined constant
2. With definition
- c₁ = e₁ ; ... ; cn : tn
§ 6.2.4 With the usual type systems.
§ 6.2.5 Incremental type checking
In situation
,----
| ? ∈ t
`----
1. Refinigning with constant c results in
,----
| c ?₁ ... ?n ∈ t
| ?₁ ∈ A₁ ... ?n ∈ An
`----
1. Refinieng with Set is an error
2. with Π is error
3. with fun, the result is
,----
| fun (lam ?₁ ?₂)
`----
§ 6.2.6 Rep. of Terms under construction
- is a tree with (nodes and) leaves being placeholders.
- a sate is like
,----
| q₁ = c₁ q11 ... q1n1
| q₂ = c₂ q21 ... q2n2
| ...
`----
plus constant declarations and definitions and constraints.
§ 6.2.7 Thin expressions
,----
| e ::= c q1 .. qn
| | Set
| | Π q q′
| | λ q'
| | q
| q' := lam q₁ q₂
`----
§ 6.2.8 Commands from a state to state
1. q := thin-e -- refinement
2. c :: thin-e -- type declaration
3. c = thin-e -- definition
4. q₁ := q₀ -- deletion; delete what's bound to q₁ and replace with q₀
§ 6.2.9 Batch type checking
too complex to understand. The goal is to simplify and understand.
§ 6.2.10 Batch checking algorithm
,----
| -- induction over G
| checkType e (G : Well typed context) : Result Ok
| checkType a G =
| Ok := checkObj a Set G
| checkType Set G = Ok
| checkType (Pi e f) G =
| Ok := checkType e G
| x := fresh G -- get a new constant in G
| Ok := checkType (apply f x) (update G x e)
| checkType (fun f) = error
| ...
`----
§ 6.2.11 Question:
In inferring type of an application (f : Pi a b)(e : a), apply b e
must reduce beta-redexes. Is this avoidable?
- Yes, if you take the closure value approach.
- B wants values to be expressions. Can't expressions be extended?
- Yes, but then you must consider their reductions too (those like
explicit substitution calculus).
§ 6.2.12 Wrap-up
- A lot of discussion on having separate worlds of expressions and
values or having values to be certain expressions.
- You can write in Haskell in the way BN wants to write with
do-notation.
- that last question above.
6.3 MT : Meta-verification and validation 16.00 - 17.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Discussed how parts of validation could be verification about
properties of formal assurance cases as objects.
§ 6.3.1 Wrap-up
Consider having composable primitives of validation / verification
activities and proving something about properties of those
combination. Cf. Simon Peyton Jones' paper "Composing contracts: an
adventure in financial engineering."
6.4 X-Sprint : 17.00 - 18.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- BN:
- JC:
- LH:
- MT: investigated the possiblities of binary distribution of Agda on
Windows independent of Haskelll Platform. There seems to be no
problems technically, as libraries seems to be all statically linked
on Windows. Statically linked GNU GMP library etc cause problems in
terms of licenses.
- YK:
7 12 May Sun.
=============
7.1 Liyang Hu : Software Transactional Memory : 09.00 - 11.40
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
§ 7.1.1 Background (1hr)
- IO monad, IORef a
,----
| data IO a = ...
| data IORef a = ...
`----
- STM monad, TVar a
,----
| data STM a = ...
| instance Monad STM where ...
| data TVar a = ...
| readTVar :: TVar a → STM a
| writeTVar :: a → TVar a → STM()
| atomically :: STM a → IO a
| retry :: STM a
| orElse :: STM a → STM a → STM a
| forkIO :: IO () → IO ()
`----
§ 7.1.2 The Language (Hutton's Razor)
- STM level
,----
| data Expression′ : Set where
| #_ : (m : ℕ) → Expression′
| _⊕_ : (a b : Expression′) → Expression′
| read : (v : Variable) → Expression′
| write : (v : Variable)(e : Expression′) → Expression′
`----
- IO level
,----
| data Expression
| #_ : (m : ℕ) → Expression
| _⊕_ : (a b : Expression) → Expression
| atomic : (e : Expression′) → Expression
`----
- No fork, but instead non-deterministic semantics.
§ 7.1.3 Heaps and Variables
,----
| postulate ∣Heap∣ : ℕ
| Heap : Set
| Heap = Vec ℕ ∣Heap∣
| Variables = Fin ∣Heap∣
`----
§ 7.1.4 1 step reduction
(↦ ~ "stop the world semantics")
,----
| data _↦′_ : Rel(Heap × Expression′)
| ↦′-⊕ℕ : ∀ {h m n} → (h , # m) ⊕ # n ↦′ (h, #(m + n))
| ...
| ↦′-read : h , reav v ↦′ h , # h[v]
| ↦′-write : h , write v (# n) ↦′ h [ v ]:= m , # m
| ...
`----
§ 7.1.5 Action
τ silent action c2 c3
§ 7.1.6 Labeled Transition System
Action → Rel(Heap × Expression)
↦-atomic : ∀ {h e h' e'} → (e↦*m : h, e ↦* h' , # m) → (c3 ▷ h ,
atomic e) ↦ (h' , # m)
↦-mutate : ∀ h' {h e} → (τ ▷ h , atomic e) ↦ (h' , atomic e)
§ 7.1.7 Transaction Log and Consistency
- Log-based implementation of transaction: read-log and wright-log
,----
| data Logs : Set where
| constrocutre _&_
| field
| ρ ω : Vec (Maybe ℕ) ∣HEap∣
|
| Write : Logs → Variables → ℕ → Logs
| Read : Heap → Logs Variable → Logs × ℕ
| -- check if you yourself have written; then return that
| .. ow, check if you have read before; then return that
| .. ow, read heap and record that fact in read log.
`----
§ 7.1.8 Consistency
,----
| Consistent: Heap → Logs → Set
| Consistent h (ρ & _) = ∀ v m → ρ [ v ] ≡ Just m → h [ v ] ≡ m
`----
Consistency is decidable - sicne Heap is finite.
,----
| Update-lookup : Heap → Logs → Variable → ℕ
| -- if you have written, what you wrote; else read from heap
| Update h l = tabulate (Update-lookup h l)
`----
§ 7.1.9 Log-Based Semantics
(↣ ~ log-based, non-stop-the-world semantics) Heap are not updated by
this one-step (write goes to log)
- STM level
,----
| data _⊢_↣′_ (h : Heap) : Rel(Logs × Expression′) where
| ...
`----
- IO level
,----
| TState = Maybe (Expression′ × Log)
| data _▷_↣_ : Action → Rel(Heap × TState × Expression)
| ....
`----
↣-mutate allows heap to be changed in anyway.
§ 7.1.10 Bisimilarity of Semantics (between ↦ version and ↣ version)
7.2 X-Sprint : All : 14.00 - 17.30
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
7.3 Wrap up
~~~~~~~~~~~
7.4 JC and MT:
~~~~~~~~~~~~~~
Discussed copatterns and termination/productivity.
7.5 YK and JC:
~~~~~~~~~~~~~~
- Looked at Agda formalisation of each other on
- Category theory, Yoneda lemma
- Normalisation by Evaluation
- Planning to put up a category theory library on a git hub.
7.6 SK
~~~~~~
Formalising Granstroem's worlds. 20% remaining.
7.7 JC and SK and MT
~~~~~~~~~~~~~~~~~~~~
Pullback. Discussed the situation of
,----
| DirectedContainer ---------> Comonad Set
| | |
| | |
| v v
| Container -----------------> Endo Set
`----
in the context of JG's Worlds.
There's a progression of
,----
| World --> Endo Set --> Mnd Set
| w ⟦w⟧ w=>_
`----
8 13 May Mon.
=============
8.1 X-Sprint, Wrap-up
~~~~~~~~~~~~~~~~~~~~~
§ 8.1.1 SK: Agda code formalising Granström's World
World, world map, composition, id, unit-laws, lifting-laws,
§ 8.1.2 LH: Discussion on formulation of bisimilarity
§ 8.1.3 JC, MT, BN: nothing to add to yesterday
§ 8.1.4 YK: Yoneda lemma and NbE for category
- NbE for monoid expression via Yoneda applied to monoids as 1-object
categories, using free monoid on "strict setoids"
- NbE for path expression of a graph free categories on a graph.
8.2 Next AIM Discussion:
~~~~~~~~~~~~~~~~~~~~~~~~
It would be good to have the next AIM in Gothenburg. BN will talk with
Ulf and Nisse about dates / place in Gothenburg to make sure they can
attend.
Page last modified on June 07, 2013, at 01:54 am
Powered by
PmWiki