Re: [Hol-info] Extension of Co-algebraic Datatype

[Michael.Norrish]

There is no documentation I’m afraid, except that the interface and behaviour 
is basically exactly the same as for IndDefLib, which is described in the 
DESCRIPTION manual.

Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Wednesday, 16 May 2018 at 06:11
To: "Norrish, Michael (Data61, Acton)" 
Cc: hol-info 
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Great!. This is exactly what I want. Thanks for helping me out...:) I located 
the file  "CoIndDefLib" in the HOL folder "src/IndDef".. Is there any 
documentation available regarding this file?

On Sun, May 13, 2018 at 6:04 AM, 
> wrote:
If you want the coinductively defined streams predicate over lllist, you can 
write

>  CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A (LCONS a 
> s)`;

<>

<>

val it =

   (⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),

⊢ ∀A streams'.

  (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒

  ∀a0. streams' a0 ⇒ streams A a0,

⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):

I think the last theorem of the triple is the cases theorem you want.

Note that if you are going to define Stream with

  Stream L = LFILTER (\n. T) L

You might as well write the equivalent

  Stream L = L

Best wishes,
Michael



From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Saturday, 12 May 2018 at 05:45

To: "Norrish, Michael (Data61, Acton)" 
>
Cc: hol-info 
>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks!. I understand that the working of LNIL and LCONS constructors since I'm 
exploring "llistTheory" for quite some time. To be very clear, I'm in the 
process of porting "stream theory" form Isabelle 
https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which 
is formalized as coinductive "stream":

codatatype (sset: 'a) stream =
  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
for
  map: smap
  rel: stream_all2

 I can see that its datatype is very similar to lazy list (llistTheory) 
datatype so rather defining a new type I defined a function that returns the 
same 'a llist-typed (lazy) list as given to its input:

∀​​L. Stream L = LFILTER (λ​​n. T) L:

type_of ``stream``;

 ``:α​​ llist -> α​​ llist``:


Later in Isabelle "stream theory", a coinductive set "streams" is defined based 
on "stream" datatype as:

coinductive_set
  streams :: "'a set ⇒​​  'a stream set"
  for A :: "'a set"
where
  Stream[intro!, simp, no_atp]: "[[a ∈​​ A; s ∈​​ streams A]] ⟹ a ## s ∈​​ 
streams A"
end

Using llistTheory functions, I'm able to define a similar function as:

∀​​A. streams A = IMAGE (λ​​a. Stream a) {llist_abs (λ​​n. SOME x) | x ∈​​ A}:

type_of ``streams``;

 ``:('a -> bool) -> 'a llist -> bool``:

However, by using shallow embedding approach, I'm not able to use some 
essential properties that are accompanied when a new coinductive datatype is 
defined. For instance, if a streams datatype is define, I may have this 
property of form:

streams.cases (Isabelle):

a ∈​​ streams A ⇒​​ (? a s. a = a ##s ⇒​​ a ∈​​ A ⇒​​ s ∈​​  streams A ⇒​​ P) 
⇒​​ P

I'm having the issues of defining these types in HOL4. Is there any way that I 
can replicate the same in HOL4?


On Mon, May 7, 2018 at 8:49 PM, 
> wrote:
You can probably define a function of that type, but you can’t define a 
*constructor* of that type for llist.   (Contrast what I’d consider to be 
llist’s standard constructors, LNIL and LCONS. They have types α llist, and α 
-> α llist -> α llist respectively.)

You said you wanted a stream type, does this mean you want a constructor for 
stream of type

  (α -> bool) -> α stream

?

Such a constructor is not recursive, so I can just write

Datatype`stream = SetConstructor (α -> bool)`

The SetConstructor term then has the desired type.

So I’m afraid I still don’t understand your question.

Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Monday, 7 May 2018 at 11:38
To: "Norrish, Michael (Data61, Acton)" 
>
Cc: hol-info 
>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks for the explanation. Let me state it clearly. Can I write down a 
constructor of type

(α -> bool) -> α​​ llist



On Sun, May 6, 2018 at 8:39 PM, 
> wrote:
I think you may be able to make your needs more precise by explicitly 
considering what your co-algebra would be.

In 

Re: [Hol-info] Extension of Co-algebraic Datatype

[Waqar Ahmad via hol-info]

Great!. This is exactly what I want. Thanks for helping me out...:) I
located the file  "CoIndDefLib" in the HOL folder "src/IndDef".. Is there
any documentation available regarding this file?

On Sun, May 13, 2018 at 6:04 AM,  wrote:

> If you want the coinductively defined streams predicate over lllist, you
> can write
>
>
>
> >  CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A
> (LCONS a s)`;
>
> <>
>
> <>
>
> val it =
>
>(⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),
>
> ⊢ ∀A streams'.
>
>   (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒
>
>   ∀a0. streams' a0 ⇒ streams A a0,
>
> ⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):
>
>
>
> I think the last theorem of the triple is the cases theorem you want.
>
>
>
> Note that if you are going to define Stream with
>
>
>
>   Stream L = LFILTER (\n. T) L
>
>
>
> You might as well write the equivalent
>
>
>
>   Stream L = L
>
>
>
> Best wishes,
>
> Michael
>
>
>
>
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Saturday, 12 May 2018 at 05:45
>
> *To: *"Norrish, Michael (Data61, Acton)" 
> *Cc: *hol-info 
> *Subject: *Re: [Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Thanks!. I understand that the working of LNIL and LCONS constructors
> since I'm exploring "llistTheory" for quite some time. To be very clear,
> I'm in the process of porting "stream theory" form Isabelle
> https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which
> is formalized as coinductive "stream":
>
>
>
> codatatype (sset: 'a) stream =
>
>   SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
>
> for
>
>   map: smap
>
>   rel: stream_all2
>
>
>
>  I can see that its datatype is very similar to lazy list (llistTheory)
> datatype so rather defining a new type I defined a function that returns
> the same 'a llist-typed (lazy) list as given to its input:
>
>
>
> *∀**​*​L. Stream L = LFILTER (*λ​*​n. T) L:
>
>
>
> type_of ``stream``;
>
>
>
>  ``:*α​*​ llist -> *α​*​ llist``:
>
>
>
>
>
> Later in Isabelle "stream theory", a coinductive set "streams" is defined
> based on "stream" datatype as:
>
>
>
> coinductive_set
>
>   streams :: "'a set *⇒**​​ * 'a stream set"
>
>   for A :: "'a set"
>
> where
>
>   Stream[intro!, simp, no_atp]: "[[a *∈**​*​ A; s *∈**​*​ streams A]] ⟹ a
> ## s *∈**​*​ streams A"
>
> end
>
>
>
> Using llistTheory functions, I'm able to define a similar function as:
>
>
>
> *∀**​*​A. streams A = IMAGE (*λ​*​a. Stream a) {llist_abs (*λ​*​n. SOME
> x) | x *∈**​*​ A}:
>
>
>
> type_of ``streams``;
>
>
>
>  ``:('a -> bool) -> 'a llist -> bool``:
>
>
>
> However, by using shallow embedding approach, I'm not able to use some
> essential properties that are accompanied when a new coinductive datatype
> is defined. For instance, if a streams datatype is define, I may have this
> property of form:
>
>
>
> streams.cases (Isabelle):
>
>
>
> a *∈**​*​ streams A *⇒**​*​ (? a s. a = a ##s *⇒**​​ a **∈**​​ A **⇒*
> *​​ s **∈**​​  *streams A *⇒**​*​ P) *⇒**​*​ P
>
>
>
> I'm having the issues of defining these types in HOL4. Is there any way
> that I can replicate the same in HOL4?
>
>
>
>
>
> On Mon, May 7, 2018 at 8:49 PM,  wrote:
>
> You can probably define a function of that type, but you can’t define a *
> *constructor** of that type for llist.   (Contrast what I’d consider to
> be llist’s standard constructors, LNIL and LCONS. They have types α llist,
> and α -> α llist -> α llist respectively.)
>
>
>
> You said you wanted a stream type, does this mean you want a constructor
> for stream of type
>
>
>
>   (α -> bool) -> α stream
>
>
>
> ?
>
>
>
> Such a constructor is not recursive, so I can just write
>
>
>
> Datatype`stream = SetConstructor (α -> bool)`
>
>
>
> The SetConstructor term then has the desired type.
>
>
>
> So I’m afraid I still don’t understand your question.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Monday, 7 May 2018 at 11:38
> *To: *"Norrish, Michael (Data61, Acton)" 
> *Cc: *hol-info 
> *Subject: *Re: [Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Thanks for the explanation. Let me state it clearly. Can I write down a
> constructor of type
>
>
>
> (*α​*​*​*​ -> bool) -> *α​*​ llist
>
>
>
>
>
>
>
> On Sun, May 6, 2018 at 8:39 PM,  wrote:
>
> I think you may be able to make your needs more precise by explicitly
> considering what your co-algebra would be.
>
>
>
> In particular, write down the type of the “general” destructor
>
>
>
>   myType -> F(myType)
>
>
>
> For lazy lists, this is
>
>
>
>   α llist -> (α # α llist) option
>
>
>
> For the co-algebraic numbers it’s
>
>
>
>   num -> num option
>
>
>
> For arbitrarily (but finite)-branching trees, it’s
>
>
>
>   Tree 

[Hol-info] [Call for Papers] Formal Verification of Physical Systems (FVPS 2018)

[Umair Siddique]

=
Workshop on Formal Verification of Physical Systems (FVPS 2018)

 August 17, 2018
  RISC, Hagenberg, Austria

   Co-located with CICM 2018

   https://easychair.org/cfp/FVPS-2018
   https://cicm-conference.org/2018/cicm.php
=



Theme
=
One of the main issues behind many failing systems is the ad-hoc
verification approach that involves a variety of formalism and techniques
for the modeling and analysis of various components of the present-age
(cyber)-physical systems. For example, control and communication protocols
are usually modeled using automata theory, and thus analyzed using model
checking techniques, while the modeling of physical aspects often requires
multivariate calculus foundations, which are in turn analyzed using
paper-and-pencil based analytical proofs, simulation or theorem proving.
The fundamental differences between these modeling and analysis techniques
limit us to analyze the whole system as one unit and thus miss many corner
cases, which arise due to the operation of all the sub-components of the
system together. One of the major concerns is that, despite the
above-mentioned evident limitation in the analysis methods, many
safety-critical systems, such as aerospace, smart-transportation,
smart-grid and e-healthcare, are increasingly involving physical elements.
Moreover, we are moving towards integrating more complex physical elements
in our engineering systems.  For example, we are moving towards Quantum
Computers to meet the high-performance needs. Similarly, phonic components
are increasingly being advocated and used in aerospace applications due to
their lightweight and temperature independency compared to traditional
electronics-based components.  Finally, the impact of physical components
is relevant to both safety and security of the overall system.  For
example, malfunction in sensor measurement may lead to safety issues
whereas sophisticated physics-based side-channel (e.g., power and acoustic
measurements) attacks lead to the security violation of the underlying
system.

The focus of the workshop will be on formal verification techniques for the
modeling, analysis and verification of safety and security critical
physical systems. We encourage submissions on interdisciplinary approaches
that bring together formal methods and techniques from other knowledge
areas such as quantum computing, control theory, biology, optimization
theory and artificial intelligence.

Topics of Interest
==
Topics of interest include (but are not limited to):

General Topics

- Formalization of mathematics and physics theories
- Interactive and automated theorem proving for physical systems
- Model Checking algorithms and tools for physical systems
- Formalization of security and safety of physical systems
- Runtime verification of safety and security properties
- Combination of formal, semiformal and infromal approaches
- Formal verification of numerical algorithms
- Refinement based verification of physical systems
- Formalization of probability, reliability and statistical metrics
- Hybrid systems
- Benchmarks for physical systems
- Formal requirement specification and validation

Application Domain
--
- Aerospace and avionic systems
- Automotive cyber physical systems
- Robotics
- Smartgrids
- Smart transportation
- Human factor modeling and analysis
- Biolgical and healthcare systems

Submission
==
Authors should prepare their papers in one column  style of CEUR-WS. There
are two categories of submissions:

- Regular papers describing developed work with theoretical results (up to
15 pages)
- Short papers on experience reports, tools or work in progress with
preliminary results (up to 6 pages)

Electronic submission is done through EasyChair. The submissions will be
reviewed by at least three PC members.  At least one author of each
accepted paper is expected to attend FVPS and presents her/his paper.

The authors of the best papers will be invited to submit extended versions
to a special issue of a Formal Methods/CPS Journal.

Important Dates
===

- Full Paper Submission: June 8, 2018
- Notification: July 6, 2018
- Camera Ready: July 13, 2018
- Workshop: August 17, 2018

Program Chairs
==
- Sofiene Tahar , Concordia University, Montreal, QC, Canada
- Osman Hasan, National University of Sciences and Technology (NUST),
Pakistan
- Umair Siddique, Waterloo Technical Center (WTC), BorgWarner, Canada

Program Committee (TBC)
==
- Aaron Dutle, NASA Langley Research Center, U.S.A.
- Jacques Fleuriot, University of Edinburgh, U.K.
- Hubert Garavel, INRIA Grenoble, France
- Atif Mashkoor, SCCH and JKU, Austria
- Sergio Mover, University of