Stream: Beginner Questions

Topic: Interpret types as lattices

waynee95 (Sep 12 2022 at 21:55):

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.

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

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

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

1. Is this even possible?
2. What's the right approach to do this?

Lukas Stevens (Sep 13 2022 at 09:01):

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.

Lukas Stevens (Sep 13 2022 at 09:05):

You could use ZFC in HOL.

waynee95 (Sep 13 2022 at 11:32):

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

Lukas Stevens (Sep 13 2022 at 11:43):

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.

Lukas Stevens (Sep 13 2022 at 11:46):

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

waynee95 (Sep 13 2022 at 11:47):

So this wouldn't exactly be an easy undertaking.

Lukas Stevens (Sep 13 2022 at 11:47):

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

Lukas Stevens (Sep 13 2022 at 11:50):

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

Lawrence Paulson (Sep 14 2022 at 14:18):

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 typehf, or possibly hf set.

waynee95 (Sep 14 2022 at 16:18):

@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: Dec 21 2024 at 16:20 UTC