# Total Denotational Semantics **URL:** \ **Category:** Links\ **Created:** [September 26, 2024, 3:28pm UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421 "2024-09-26T15:28:14Z")\ **Posts on this page:** 20\ **Page:** 1

**Author:** ![sgraf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sgraf/32/392_2.png) [@sgraf](https://discourse.haskell.org/u/sgraf)\ **Post date:** [September 26, 2024, 3:28pm UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/1 "2024-09-26T15:28:14Z")

I finally overhauled my blog (it just took a PhD worth of time) and published a new blog post, using Haskell to make denotational semantics executable: [fixpt · Total Denotational Semantics](https://fixpt.de/blog/2024-09-23-total-denotational-semantics.html) I tried to make the matter accessible to people with at least a bit of background in formal semantics, so I apologise to anyone who does not share this background. Let me know what you think! ---

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\ **Post date:** [September 26, 2024, 7:14pm UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/2 "2024-09-26T19:14:24Z")

As long as we’re only interested in total executable denotational semantics (and not proving properties of the semantics), couldn’t we achieve the same with Liquid Haskell’s termination checker and the ideas from Conor’s [“Productive Coprogramming with Guarded Recursion”](https://bentnib.org/productive.pdf)? Just define the guarded fixed point in an “unsafe” module with the termination checker disabled. ---

**Author:** ![olf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/olf/32/3813_2.png) [@olf](https://discourse.haskell.org/u/olf)\ **Post date:** [September 26, 2024, 8:15pm UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/3 "2024-09-26T20:15:34Z")

First of all: Respect for being able to condense a PhD thesis into such a short blog post. What I find intriguing about the attempt to provide semantics in Haskell is that (a large subset of) _Haskell has domain semantics_ itself, so you are embedding a domain (the semantic domain of the lambda calculus) into another domain (the semantic domain of the Haskell type), but in a way that is not order-preserving. In a way, it is an _orthogonal_ embedding because the Haskell domain now has a second partial order that is unrelated to the specialization order. For example, we could say `Bot <= Fun id` and that relation is _decidable_, while the two elements are not comparable by ⊑. Your total semantics is mapping the lambda calculus (or whatever language) to a subset of total elements of this bi-ordered domain, and on this subset the specialization order is flat. An “execution” on such a structure is a map that translates the orthogonal order into ⊑. For example it maps both the syntactically divergent `diverge = fix Step` as well as `Stuck` to the properly divergent ⊥. For extra fun, observe that `Exp` itself is a domain, and you have only considered the total elements of it. In fact, `denot` also translates the partial elements of `Exp` to partial elements of `D`. I do not know a mathematical theory of such structures; it must be bi-topological. It sounds like a wonderful rabbit hole to fall into. You say that while the mathematical interpreter _I_ is total, the naive `interp` is not. The latter is easily seen, but how does one prove the former? I would challenge your notion of totality and say that _the denotational semantics of_ `interp` is just as total as your interpreter _I_ because it maps every lambda term to a well-defined element of the semantic domain of `D`, of which ⊥ is a member. ---

**Author:** ![olf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/olf/32/3813_2.png) [@olf](https://discourse.haskell.org/u/olf)\ **Post date:** [September 26, 2024, 8:43pm UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/4 "2024-09-26T20:43:01Z")

A more geometric example of a bi-ordered domain and total semantics: Consider the domain D of closed sub-intervals of the unit interval [0,1], ordered by reverse inclusion: [a,b] ⊑ [x,y] if a ≤ x and y ≤ b. The numbers in [0,1] are embedded as singleton intervals at the top of this domain. Can we extend the usual order ≤ of numbers to the entire domain, in a way so that [0,0] is least and [1,1] is greatest? Indeed we can: Say that [a,b] ≤ [x,y] if a ≤ x and b ≤ y. (This is the _may_ modality.) In fact both orders render this domain a bounded complete distributive lattice, and the lattice operations distribute over another. The complete lattice ([0,1],≤) is a sub-lattice of the complete lattice (D,≤). ---

**Author:** ![Lysxia](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/lysxia/32/2916_2.png) [@Lysxia](https://discourse.haskell.org/u/Lysxia)\ **Post date:** [September 26, 2024, 9:30pm UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/5 "2024-09-26T21:30:15Z")

Very fun post. With so many layers of partiality, you’re in for a loop. ---

**Author:** ![atravers](https://avatars.discourse-cdn.com/v4/letter/a/45deac/32.png) [@atravers](https://discourse.haskell.org/u/atravers)\ **Post date:** [September 27, 2024, 2:14am UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/6 "2024-09-27T02:14:19Z")

To avoid the hassle of hauling an abstract heap throughout their semantics (monadically or otherwise), Jennifer Hackett and Graham Hutton used a different technique: - [Call-by-Need Is Clairvoyant Call-by-Value](https://www.cs.nott.ac.uk/~pszjlh/cbncbv.pdf) ([erratum](https://www.cs.nott.ac.uk/~pszjlh/cbncbv_erratum.pdf)) Perhaps it can help to alleviate the need for **\>\>=** appearing in your semantics (e.g. _D_ ⟦⋅⟧)… ---

**``** Partiality is inescapable: - Roads, bridges and cranes have maximum load/weight limits - exceeding them results in damage and possibly collapse. - Water and gas pipes (along with [submersibles](https://www.whoi.edu/multimedia/remembering-nereus/)) have maximum pressure limits, with similar consequences when exceeded. - Insulated electrical cables and electronic components have maximum voltage limits. - Even superconductors [have maximum limits](https://cds.cern.ch/record/970378/files/cer-002634909.pdf) on electrical current. So this ~~_obsesession_~~ fascination with totality for software completely eludes me - even if you could stomp every last bug out of existence from your programs using types, the Universe in which said programs reside contains _cosmic radiation_ which can not only change nucleotides, but bits of information as well (be it data or code). What was bug-free yesterday could still crash tomorrow. _“But it makes the maths easier!”_ So would pretending zero doesn’t exist. But it does: 1. Place one bead in a bowl. 2. Take one bead from same bowl. 3. How many beads are left in that bowl? **`Zero`** (and perhaps an empty round container was the inspiration for its numerical/symbolic representation, **`0`** ). There’s also the [bemusing attempts](http://discourse.haskell.org/t/in-retrospect-was-burning-bridges-a-mistake/8188/35) to avoid the problems associated with the actual existence of zero: > [@](#): > > The standard division function on natural numbers in Coq, `div`, is total and pure, but incorrect: when the divisor is 0, the result is 0. > > [Gradual Certiﬁed Programming in Coq](https://arxiv.org/pdf/1506.04205) (page 8 of 15). Static types are alright _when you’re not having to constantly type them out_ - it’s **so** much nicer to just write: ```haskell midpoint x y = (x + y) / 2 ``` instead of: ```haskell double midpoint (double x, double y) { return (x + y) / 2; } ``` But now the goal is to explicate _every last detail_ of what the definitions in our programs should do using types, to the point of implementing fully-formed proofs! So what prevents bugs from sneaking into said types and proofs (particularly as Haskell’s type system has been Turing-complete since the advent of functional dependencies)? It’s just extra code; the bugs aren’t fussy! [![](https://imgs.xkcd.com/comics/shouldnt_be_hard.png) ](https://imgs.xkcd.com/comics/shouldnt_be_hard.png) If too many perceive Haskell as _“being hard”_ (e.g. poor benefit/cost ratio), then the blowtorch is optional: there are many other programming languages out there: - old ones: - and new: **``** ---

**Author:** ![olf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/olf/32/3813_2.png) [@olf](https://discourse.haskell.org/u/olf)\ **Post date:** [September 27, 2024, 5:58am UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/8 "2024-09-27T05:58:52Z")

With other denotational semantics one usually proves that the semantic category is closed under all necessary type constructions, such as sums, products and certain fixed points. Can you do that with total semantics? For flat types `t`, it seems okay to add a new distinguishable bottom and nothing else: ```haskell Denot t = Bottom | Total !t ``` Do we also need a non-strict `Step` constructor here? For recursive types, say `r = Fix f`, the construction laid out in your blog post seems adequate: ```haskell data BottomT f a = Stuck | Now !(f a) | Delay (f a) type Denot r = Fix (BottomT f) ``` Here the constructor `Now` plays the role of `Ret` and `Delay` plays the role of `Step`. What I called “execution” above now becomes a function `Denot t -> t`. Since `Denot r` is again a fixed point, we can iterate the construction. By tacking on an extra layer of `Now` we obtain a function `Denot r -> Denot (Denot r)` that preserves total elements so chances are this is a comonad. The flat case is subsumed in `BottomT` because `t` is the fixed point of `Const t`. ---

**Author:** ![olf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/olf/32/3813_2.png) [@olf](https://discourse.haskell.org/u/olf)\ **Post date:** [September 27, 2024, 7:26am UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/9 "2024-09-27T07:26:17Z")

> [@atravers](#): > > So this ~~_obsesession_~~ fascination with totality for software completely eludes me While I agree that ignoring or eradicating the existence of partiality leads us nowhere, I think there is still value in this total semantics: The advantage is that in the total semantics the specialization order ⊑ (of the original type whose denotation we study) becomes a decidable relation ≤, so one can perform analyses that otherwise would be forbidden by Rice’s theorem. ---

**Author:** ![sgraf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sgraf/32/392_2.png) [@sgraf](https://discourse.haskell.org/u/sgraf)\ **Post date:** [September 27, 2024, 10:54am UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/10 "2024-09-27T10:54:07Z")

Hmm. It is a bit unclear to me what exactly you mean. Perhaps let me try to provide a non-answer with an explanation of how I think Liquid Haskell could work with guarded recursion. First off, you can simply postulate the (singly-clocked) Later modality as ```haskell newtype Later a = MkLater a deriving (Functor, Applicative) via Identity -- perhaps got DerivingVia wrong here; you get the idea ``` Then export `Later`, but not `MkLater`. I think this is the “unsafe” runtime system module that you are referring to. (You likely need more primitives besides `Applicative` that can be proven safe in the underlying topos model.) Then you define the general guarded recursion fixpoint combinator as follows (i.e. it it _not_ primitive!) ```haskell gfix :: (Later a -> a) -> a gfix f = f (pure (gfix f)) -- NB: this is safe ``` However, `gfix` enables the definition of infinite, non-well-founded structures. I have my doubts that Liquid Haskell’s termination checker would be happy about this if it keeps unfolding `MkLater`. [This paper indicates that it currently is not happy, and suggests step-indexed induction as a model of coinduction](https://nikivazou.github.io/static/Haskell22/coinduction.pdf). I think that solves two out of three problems best thought separately: 1. Soundness in the presence of non-well-founded codata 2. A way to do coinductive proofs by integrating productivity checks into the (refined) language 3. A way to do coinductive proofs by way of doing a step-indexed proof in an underlying step-indexed inductive model of coinduction. As far as I can tell, the paper solves (1) (don’t pass `--no-adt`) and (3) (I wonder how this is compatible with `--adt`?? They do not seem to step-index the data types!), but not (2). Instead of providing a productivity checker, it relies on the user to do step-indexing. That’s well and good for simple first-order types such as streams with a simple encoding of observational equality, but is unlikely to work well for higher-order, negatively recursive types such as `Value`. * * * **Problem 1** : What does it take to make LH sound wrt. the Later modality? I think it suffices to prevent LH from deriving an induction principle for `Later` (so LH must know about it). That is, following `P a` from `P (Later a)` is **utterly** unsafe and we need to hide this “implementation” from LH. One way to achieve this is to keep `Later` opaque and tell the SMT solver just about the applicative laws (such as `pure f <*> pure a = pure (f a)`), but not about how `pure` and `<*>` are implemented. * * * To understand the qualitative difference between Problem 2 and Problem 3, let me give an analogy. I think we agree that programming in C is more convenient than programming in assembler. Among other things, the C compiler ensures a proper stack and register discipline (you don’t need to “prove” that your program adheres to this discipline). But sometimes writing C is “not enough” and you really need to write assembler, for example when writing an operating system kernel or a driver, because the C language does not offer the necessary low-level, architecture-specific abstractions. By analogy, proving in a guarded type system is more convenient than proving in the underlying (step-indexed or Scott) topos model directly. You can simply forget about the mathematical details of the underlying model and live in your axiomatised world (“each function call gets fresh local variable slots”). This argument is similar to the argument of blog post that reasoning on discretely-ordered total elements is more convenient than on partial ones. Sometimes (rather frequently, actually), staying within the applicative functor interface/DSL/internal language of the Later modality is insufficient. (I think [this is an example](https://github.com/sgraf812/abs-den/blob/22a8fd1f577d12596bf53257d27d983054358173/agda/Concrete.agda#L260).) In this case, you really need to unpack the underlying model and attempt a step-indexed proof for the primitive that you need (called `flip-tick` in my example). * * * So, problems (2) and (3) are about writing convenient and useful tools to write coinductive proofs. (2) is more about high-level convenience and (3) is about the “assembler to make it happen” if (2) is insufficient. **Problem 2** : How do we write convenient LH proofs involving Later? I think we would need to teach LH about _Löb induction_, which is `gfix` generalised to `a :: Prop`. That would probably allow you to do all kinds of proofs about programs in the Applicative fragment. (I believe the main benefit of _Ticked_ Cubical Type Theory is that the Applicative reasoning becomes part of definitional equality, so you don’t need to do proofs involving Applicative laws.) This would not be too much work, I think. At this point, LH would be on par with the (admittedly still infant and mediocre, if I may say so) treatment of guarded types in Agda, Rocq or Lean, where you axiomatise all combinators and equational theory. I you want more combinators than just Applicative (and you likely will), then you need more axioms that describe how these combinators can be used safely. I think you can do this by introducing new uninterpreted functions for combinators and `assume` axioms about their equational theory. For simple kinds of combinators, this might work well, because the axioms are “obviously true”. However, every axiom is a source of unsoundness unless you have proved it. **Problem 3** is about providing users a way to prove correct their axioms in an underlying topos model. (Semanticists like Jon Sterling tend to do these proofs on paper. I believe that is for lack of a good solution to this problem in today’s proof assistants.) In order for that to work, LH would need to reflect the Haskell definition of the combinator and the definition of the axiom into this topos model (via a denotational semantics, from Haskell into a suitable Haskell DSL backed by SMT logic) and let the user provide a proof there. Finding the right Haskell DSL here is the subject of synthetic guarded domain theory (= axiomatisation of an adequate topos), if I understand correctly; an active research area. ---

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\ **Post date:** [September 27, 2024, 11:01am UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/11 "2024-09-27T11:01:13Z")

Thanks for your extensive response! > [@sgraf](#): > > Hmm. It is a bit unclear to me what exactly you mean. I had this lying around and now uploaded it to GitHub: [GitHub - noughtmare/coprogramming: Implementation of McBride's productive coprogramming + liquid haskell termination checking](https://github.com/noughtmare/coprogramming) Check out `src/Control/Coprogramming.hs` for the primitives and `app/Main.hs` for how they can be used (hopefully) safely with Liquid Haskell’s termination checker to implement `repmin` (please ignore the other things in that file). > [@sgraf](#): > > `gfix f = f (pure (gfix f)) -- NB: this is safe` I don’t think liquid haskell’s termination checker can see that it is safe. > [@sgraf](#): > > [This paper indicates that it currently is not happy, and suggests step-indexed induction as a model of coinduction](https://nikivazou.github.io/static/Haskell22/coinduction.pdf) > [@sgraf](#): > > That is, following `P a` from `P (Later a)` is **utterly** unsafe and we need to hide this “implementation” from LH. To be clear, I only meant that we could use LH’s termination checker, not to use the actual proof mechanism that LH provides. I think that sidesteps all these issues, because AFAIK the termination checker is purely syntactic. > [@sgraf](#): > > However, `gfix` enables the definition of infinite, non-well-founded structures. Do you have an example? Ah, I guess you could define an infinite stream like in my `app/Main.hs` file. However, that stream will contain an infinite amount of `Later`s which you can never `force` all the way. So, termination is still preserved as far as I can tell. ---

**Author:** ![sgraf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sgraf/32/392_2.png) [@sgraf](https://discourse.haskell.org/u/sgraf)\ **Post date:** [September 27, 2024, 11:10am UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/12 "2024-09-27T11:10:35Z")

> First of all: Respect for being able to condense a PhD thesis into such a short blog post. Thank you, but I would not say that what I discuss in the post is part of my thesis, which is about static analyses such as found in GHC. With “(it just took a PhD worth of time)” I was trying to say that I had neglected by blog for almost my entire PhD. > You say that while the mathematical interpreter _I_ is total, the naive `interp` is not. The latter is easily seen, but how does one prove the former? If it weren’t total, it would not be a function 🙂 More seriously, it’s composed from total primitives, so it must be total as well. (That’s kind of the point of domain theory.) > I would challenge your notion of totality and say that _the denotational semantics of_ `interp` is just as total as your interpreter _I_ because it maps every lambda term to a well-defined element of the semantic domain of `D`, of which ⊥ is a member. Well, of course the denotational semantics of the Haskell program `interp` is a total function; it’s a denotational semantics after all! But there is an important difference: The semantics do not coincide in the way I think you imply. For _I_, we have `I[[Ω]] emp = ⊥ = I[[x]] emp`. On the other hand, if we had a denotational semantics for Haskell `[[e]]`, then surely `[[interp omega Map.empty]] = ⊥`, whereas `[[interp (Var "x") Map.empty]] = lift Bot`. Note that `Bot` is a data constructor! It is never `lift Bot = ⊥`. This means you cannot reason about the object language without knowing the denotational semantics of the meta language Haskell (rather than just its equational theory) as well. It is one of the main consequences I had hoped to convey with the post! ---

**Author:** ![sgraf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sgraf/32/392_2.png) [@sgraf](https://discourse.haskell.org/u/sgraf)\ **Post date:** [September 27, 2024, 11:31am UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/13 "2024-09-27T11:31:36Z")

> [@jaror](#): > > I don’t think liquid haskell’s termination checker can see that it is safe. Indeed, that’s correct. Is that termination checker part of LH or of the SMT solver? That is, can you just deactivate the termination check on this function? I guess my point is that it’s fine to reflect this definition into the logic, whereas it would not be fine to reflect the definition of `Later` into the logic. I’m positively sure that you _will_ need to reflect `gfix` into the logic or at least provide it as an equality for manual unwrapping. How else would you do proofs about `gfix`? > [@jaror](#): > > Do you have an example? Hmm, only if unwrap `MkLater`, which I think is your point? But it is also my point above: ```hs data Stream a = a :> Later (Stream a) ones :: Stream Int ones = gfix (\r -> 1 :> r) false :: Void false = go ones where go (_ :> MkLater r) = go r ``` I’ve not used LH, but the [paper](https://nikivazou.github.io/static/Haskell22/coinduction.pdf) uses a similar counterexample in 1.3 (albeit using `--no-adt` without which `Stream` would not be possible to define.) > [@jaror](#): > > Check out `src/Control/Coprogramming.hs` for the primitives and `app/Main.hs` for how they can be used (hopefully) safely with Liquid Haskell’s termination checker That’s quite nice! And you hide the `L` constructor as well, which makes it safe. But I’m not sure if you will manage to prove any properties about `repmin` if you don’t reflect `gfix` into the SMT logic. ---

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\ **Post date:** [September 27, 2024, 11:33am UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/14 "2024-09-27T11:33:45Z")

> [@sgraf](#): > > How else would you do proofs about `gfix`? Ah, I meant to say I don’t want to do proofs. I just want to be sure my programs terminate. That’s what I meant with: > [@jaror](#): > > As long as we’re only interested in total executable denotational semantics (and not proving properties of the semantics) ---

**Author:** ![olf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/olf/32/3813_2.png) [@olf](https://discourse.haskell.org/u/olf)\ **Post date:** [September 27, 2024, 11:34am UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/15 "2024-09-27T11:34:25Z")

> [@sgraf](#): > > The semantics do not coincide in the way I think you imply. Oh, I did not mean to claim that _I_ and _iterp_ are semantically equivalent. After all, isn’t the whole point of the exercise that they aren’t? ---

**Author:** ![atravers](https://avatars.discourse-cdn.com/v4/letter/a/45deac/32.png) [@atravers](https://discourse.haskell.org/u/atravers)\ **Post date:** [September 27, 2024, 12:12pm UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/16 "2024-09-27T12:12:00Z")

> [@jaror](#): > > Ah, I meant to say I don’t want to do proofs. I just want to be sure my programs terminate. Perhaps you can have both: > [@](#): > > A functional big-step semantics is essentially an interpreter written in a purely functional style and equipped with a clock to ensure that the function is total, even when run on diverging programs. Hence the interpreter can be used in a higher-order logic of total functions – the kind supported by Coq, HOL4, and Isabelle/HOL – as a formal deﬁnition of the semantics. In this way, it harkens back to Reynolds’ idea of [deﬁnitional interpreters](https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/reynolds-definitional-interpreters-1998.pdf) to give a readable account of a semantics. Additionally, by initialising the clock to a very large number, the same functional big-step semantics used for proof can also be executed on test programs for exploration and validation. > > [Functional Big-step Semantics](https://cakeml.org/esop16.pdf) (page 2 of 27) ---

**Author:** ![sgraf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sgraf/32/392_2.png) [@sgraf](https://discourse.haskell.org/u/sgraf)\ **Post date:** [September 27, 2024, 3:44pm UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/17 "2024-09-27T15:44:28Z")

> [@jaror](#): > > Ah, I meant to say I don’t want to do proofs. I just want to be sure my programs terminate. Ah, yes. Using LH to prove that your definitions are total is quite a neat idea! _However_, you still need to teach LH about what kind of data type definitions are OK. For example, the original definition of `D` from the post is not. That is, `data D = Fun (D -> D) | Stuck` is probably rejected by LH’s totality checker. However, it should better allow `data Stream a = a :> Later (Stream a)` and `data D = Fun (Later D -> D) | Stuck`! ---

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\ **Post date:** [September 30, 2024, 7:44pm UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/18 "2024-09-30T19:44:02Z")

I would have expected the denotation of `res_omega` to be an infinite nesting of `step` constructors. However, when normalizing it in Agda, I got a surprisingly finite, but unintelligible, result. Was my intuition wrong and what does that normal form really tell us? ---

**Author:** ![sgraf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sgraf/32/392_2.png) [@sgraf](https://discourse.haskell.org/u/sgraf)\ **Post date:** [September 30, 2024, 8:09pm UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/19 "2024-09-30T20:09:12Z")

I don’t think it normalises through transports, but I could be wrong about that. At least it looked like some transports were getting in the way of beta redexes when I checked the output a couple of days ago. It’s strange that it does not appear to normalise through transports, because I had thought that was the main point about cubical… ---

**Author:** ![sgraf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sgraf/32/392_2.png) [@sgraf](https://discourse.haskell.org/u/sgraf)\ **Post date:** [September 30, 2024, 8:14pm UTC](https://discourse.haskell.org/t/total-denotational-semantics/10421/20 "2024-09-30T20:14:56Z")

At any rate, as you have probably guessed, normalising through the transport that unfolds fix leads to undecidable defn. equality. So that’s perhaps why it doesn’t completely normalise. [Next page](https://discourse.haskell.org/t/total-denotational-semantics/10421.md?page=2)