Are denotational semantic mappings decidable?

Question

Apologies for my poor expression of this question, I'm not sure I have the vocabulary to ask it appropriately.

I've written (very recently) something akin to

⟦let x = x in x⟧ = ⊥

but really I'm failing to understand something tricky here. I can assert that this statement is truly ⊥ because I know it's a non-productive infinite loop. Furthermore, I can assert something like

⟦let ones = 1:ones in ones⟧ = μ(λx.(1,x)) = (1, (1, (1, ... )))

but what goes into that elipsis? Presumably it's an infinite number of "1-and-tuples", a perfectly well-defined mathematical object if you're alright with the AFA, but how can I convince you that it's not some finite number of "1-and-tuples" and then a non-productive ⊥?

Obviously, this involves answering the halting problem, so I can't in general.

So in that case, how can we compute semantic mappings as if they're a total function? Are semantics necessarily non-deterministic for Turing-incomplete languages? I imagine it means that semantics are always only ever an approximate, informal description of a language, but does this "hole" go further?

Answer 1

There are no set theoretic models of turing complete languages. If your language is strongly normalizing, there exits a total function to "interpret it" to something. You may or may not have set theoretic semantics in a non-turing complete language. Regardless, turing complete, and non-turing complete, languages can have non set theoretic semantics with total semantic mapping functions.

I don't think that is the issue here.

There is a difference between inductive and co-inductive definitions. We can explore this set theoretically:

The inductive definition of a list of integers reads:

the set [Z] is the smallest set S such that the empty list is in S , and such that for any ls in S and n in Z the pair (n,ls) in S.

This can also be presented in a "step indexed" way as [Z](0) = {[]} and [Z](n) = {(n,ls) | n \in Z, ls \in [Z](n-1)} which lets you define [Z] = \Union_{i \in N}([Z](n) (if you believe in natural numbers!)

On the other hand, "lists" in Haskell are more closely related to "coinductive streams" which are defined coinductively

the set [Z] (coinductive) is the largest set S such that forall x in S, x = [] or x = (n,ls) with n in Z and ls in S.

That is, coinductive defintions are backwards. While inductive definations define the smallest set containing some elements, coinductive definations define the largest set where all elements take a certain form.

It is easy to show that all inductive lists have finite length, while some coinductive lists are infinitely long. Your example requires coinduction.

More generally, inductive definitions can be though of as the "least fix-point of a functor" while coinductive definitions can be thought of as "the greatest fix-point of a functor". The "least fix point" of a functor being just its "initial algebra" while the "greatest fixpoint" is its "final coalgebra". Using this as your semantic tools makes it easier to define things in categories other than the category of sets.

I find that Haskell provides a good language for describing these functors

data ListGenerator a r = Cons a r | Nil

instance Functor (ListGenerator a) where
  fmap f (Cons a x) = Cons a (f x)
  fmap _ Nil        = Nil

although haskell provides a good language for describing these functors, because its function space is CBN and the language is not total, we have no way of defining the kind of least fix point we would like :(, although we do get the definition of the greatest fixpoint

data GF f = GF (f (GF f))

or the non recursive existentially quantified

data GF f = forall r. GF r (r -> (f r))

if we were working in a strict or total language, the least fixpoint would be the universally quantified

data LF f = LF (forall r. (f r -> r) -> r)

EDIT: since "smallest" is a set theoretic notion though the "least"/"greatest" distinction might not be the right one. The definition of LF is basically isomorphic to GF and is "the free initial algebra" which is the categorical formalism of "least fix point."

as to

how can I convince you that it's not some finite number of "1-and-tuples" and then a non-productive ⊥?

you can't unless I believe in the kind of constructions in this post. If I do, then your definition leaves me stuck!. If you say "ones is the coinductive stream consisting of the pair (1,ones)" then I have to believe! I know ones is not _|_ by definition, and thus by induction I can show that it can't be the case that for any value n I have n ones and then bottom. I can try to deny your claim only be denying the existence of coinductive steams.

Answer 2

For more on proof techniques over coinductive structures (expanding on Philip JF's very nice answer), you can take a look at Hinze and James' "Proving the Unique Fixed-Point Principle Correct": http://www.cs.ox.ac.uk/people/daniel.james/unique/unique-tech.pdf