Stream: Beginner Questions

Topic: 'a option vs underspecified

Robert Soeldner (May 08 2021 at 06:35):

Hi,

so-far I have used a record like (node\edge are type_synonyms to nat)

record ('a,'v,'e) graph =
  nodes :: "node set"
  edges :: "edge set"
  src   :: "edge ⇒ node"
  trg   :: "edge ⇒ node"
 ...

to describe a graph. Checking the well-formedness was performed by (∀ x ∈ (edges gr) . src gr x ∈ nodes gr ∧ trg gr x ∈ nodes gr) ....

When specifying a concrete graph, I tried naively tried

 ⦇nodes = {1,2}, edges={1},
                 src = [1 ↦ 1],
                 trg = [1 ↦ 1],
                 ...

which forces src\trg to be of type edge => node option.
I read about underspecifying https://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total%2C_sometimes_undefined and thought, this is ok for my usage but now I"m not sure if I fully understood the topic.

Does it make sense for src\trg to map to 'a option if a well-formed graph permits this case?

Robert Soeldner (May 08 2021 at 08:43):

(deleted)

Jakub Kądziołka (May 08 2021 at 11:17):

the [1 ↦ 1] syntax models partiality explicitly with the option datatype. If you want to define a function by specifying its values at specific points and leaving the rest undefined, you could use (%x. undefined)(1 := 1) (this is called the functional update syntax; the % is the ASCII symbol for lambda which I don't have a way of typing here)

Jakub Kądziołka (May 08 2021 at 11:18):

As for what makes sense for modeling a graph, I'd probably use edges :: "(node, node) set" (or a multiset, depends on the requirement)

Robert Soeldner (May 08 2021 at 16:52):

thank you for the fast reply. I will check both approaches :-)

Lukas Stevens (May 08 2021 at 19:33):

Btw. there is already a similar graph library: https://www.isa-afp.org/entries/Graph_Theory.html
Furthermore, @Mohammad Abdulaziz is currently working on a graph library which aims to unify the different representations that currently exist in Isabelle: https://github.com/wimmers/archive-of-graph-formalizations/pull/1

Robert Soeldner (May 08 2021 at 20:01):

this is good to know, thank you for pointing me to it.

Last updated: Dec 21 2024 at 16:20 UTC