<div dir="ltr">Dear Iris Club,<div><br></div><div>I would like to ask a question which is not really directly related to the end users of the logic.. :-)</div><div><br></div><div><br></div><div>I think one of the design principle behind the Iris logic is constructivism, because:</div><div><br></div><div>- In the ICFP 2016 paper is said "Dockins et al. introduced multi-unit separation algebras [14], which, unlike PCMs, only demand the existence of a possibly different unit ua with ua · a = a for any element a. A crucial difference between multi-unit separation algebras and RAs is that we present the monoidal operation and core as a function, whereas they represent these as relations."  I think the reason the authors think function and relation have a crucial difference is, they care constructivism.</div><div><br></div><div>- In the Iris 2.0 documentation, a COFE is defined as a tuple of the form (T, =_n, lim: chain(T) -> T).  It is stronger than requiring just existence of the limit; it actually requires a function that maps a chain to its limit.</div><div><br></div><div><br></div><div>My question is: is this constructivism necessary in the development of the Iris logic?  Or is it a preference?</div><div>    - A subquestion is: is the constructivism related to the freedom from all the axioms in the development?</div><div>    - A remark: it seems that constructivism is applied somewhere, and isn't elsewhere.  For example the (CMRA-extend) rule merely requires the existence of the decomposition, and not the construction of the decomposition.</div><div><br></div><div><div><br></div><div>Thank you,</div><div>Jeehoon</div><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>
</div></div>