## 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?

(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: Jul 15 2022 at 23:21 UTC