[Iris-Club] Constructivism: necessity or preference?

[Jeehoon Kang]

Dear Iris Club,

I would like to ask a question which is not really directly related to the
end users of the logic.. :-)


I think one of the design principle behind the Iris logic is
constructivism, because:

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

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


My question is: is this constructivism necessary in the development of the
Iris logic?  Or is it a preference?
    - A subquestion is: is the constructivism related to the freedom from
all the axioms in the development?
    - 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.


Thank you,
Jeehoon

-- 
Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
Software Foundations Laboratory <http://sf.snu.ac.kr>
Seoul National University <http://www.snu.ac.kr>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20160814/b54a97e8/attachment.html>