I am trying to formalize something that's essentially a typed LC with fixpoint operators and I am a bit stuck on how to approach this in Isabelle.

Types are defined over some base type denoted by the diamond

$\tau ::= \blacklozenge \mid \tau^v \rightarrow \tau \\ v ::= + \mid - \mid \pm$

The v-annotations are variances and specify the dependency of the values of a function on their arguments. Plus indicates monotonic behavior, minus is antitonic and plusminus indicates unspecified.

Before continuing with defining terms and semantics for terms, one needs to define how these types are interpreted. The idea is, given a finite lattice M, we associate for each type tau, a finite lattice M_tau.

The base type is interpreted as the given lattice

$[\![ \blacklozenge ]\!]^\mathcal{M} := \mathcal{M}$

and function types are interpreted as

$[\![ \tau_1^v \rightarrow \tau_2 ]\!]^\mathcal{M} := ([\![ \tau_1 ]\!]^\mathcal{M})^v \rightarrow [\![ \tau_2 ]\!]^\mathcal{M}$

So I started with

```
datatype variance =
Plus
| Minus
| PlusMinus
datatype ty =
Base
| Fun ty variance ty
```

But now I am stuck with how to define the interpretation as mentioned above.

- I tried to write a function for the semantics of types
`sem_ty`

```
fun make_lattice :: "'a::finite_lattice ⇒ 'a::finite_lattice ⇒ 'a::finite_lattice" where
"make_lattice M1 M2 = undefined"
fun apply_variance_to_lattice :: "'a::finite_lattice ⇒ variance ⇒ 'a::finite_lattice" where
"apply_variance_to_lattice M v = undefined"
fun sem_ty :: "ty ⇒ 'a::finite_lattice ⇒ 'a::finite_lattice" where
"sem_ty Base ℳ = ℳ" |
"sem_ty (Fun ty1 v ty2) ℳ =
(let M1 = sem_ty ty1 ℳ in
let M2 = sem_ty ty2 ℳ in
make_lattice (apply_variance_to_lattice M1 v) M2)"
```

But I am not sure how to define the two missing functions. It would also be a problem that both return the same type, since that wouldn't actually be the case but using a different type variable, doesn't work.

- Another idea was that this the wrong direction and I need to use

```
instantiation ty :: finite_lattice
```

But here I wasn't sure how to get the base lattice incorporated.

- Another idea was that I define another datatype
`sem_ty`

that describes the semantics of the`ty`

datatype and resembles the associated lattice but that also didn't get me far.

So that leaves me with a few questions...

- Is this even possible?
- What's the right approach to do this?

The problem here is that the type of the output fundamentally depends on the input term (each additional function arrow changes the type). You can't represent this in the type system of Isabelle/HOL.

You could use ZFC in HOL.

@Lukas Stevens Thanks for the comment.

So a theorem prover based on dependent type theory would be able to formalize the interpretation function?

I am not familar with ZFC in HOL. Is there are any documentation that would help?

How would it help in this matter? Not too familiar with ZFC.

Yes, if you have dependent types you can represent this. There is an article by Larry that gives some context to this AFP entry.

Using ZFC in HOL, you could represent your functions as sets of pairs. The entry defines a hierarchy of sets represented as single type `V`

. This type accomodates all small sets so you should be able to represent any suitably constrained function as a set of type `V`

.

The trouble is that there is no theory of functions for ZFC in HOL, as far as I know.

So this wouldn't exactly be an easy undertaking.

Difficult to say. The basics shouldn't be very hard.

Maybe @Lawrence Paulson could comment on this since he authored the entry?

In order to approach this problem you need to be clearer about the interpretation of your types. You seem to imply that they are all finite lattices. Then I believe that restricting yourself to the lattice determined by the subset relation is sufficient to represent all finite lattices. If that is correct, then you don't even need to leave the confines of higher-order logic and can interpret your types within the hereditarily finite sets.

You haven't specified what is involved in creating a finite lattice from two other finite lattices corresponding to the function space. You also haven't specified what it means to apply a variance to a lattice. It's impossible to formalise a definition without knowing what the definition is.

I don't think your issues have anything to do with types. If it is possible to use the hereditarily finite sets, all of your lattices can have type`hf`

, or possibly `hf set`

.

@Lawrence Paulson Thanks for your comment! Yes I did leave out a few details.

$\text{Let } \mathcal{M} := (M, \leq) \text{ be a complete lattice. Then we have } \mathcal{M}^- := (M, \geq), \text{ where } x \geq y \iff y \leq x. \mathcal{M}^+ := (M, \leq).$

So a negative variance applied to a lattice, yields a reversed order and positive variance preserves the order. Both operations preserve being a lattice and also completeness.

For the unspecified variance, we get

$\mathcal{M}^\pm := (M, =), \text{ where = denotes equality}.$

In this case this operation does not yield a lattice in general.

Lastly, we have

$\text{Let } \mathcal{M}_i := (M_i, \leq_i), \; i \in \{1,2\} \text{ be complete lattices. Then we have } \mathcal{M}_1 \rightarrow \mathcal{M}_2 := \{ f : M_1 \rightarrow M_2 \mid f \text{ is monotonic}\}, \sqsubseteq), \text{ where } f \sqsubseteq g \text{ if } f(x) \leq_2 g(x), \forall x \in M_1.$

This is the lattice of component-wise orderd functions from M_1 to M_2 and it is complete if the \mathcal{M}_2 lattice is complete.

The interpreation of the types using these constructions yields a complete lattice, since the only breaking operation is only used on the argument side of the function operator. And if the base lattice is finite, then so is the resulting lattice.

Last updated: Sep 11 2024 at 16:22 UTC