Denotational semantics is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called denotations) that describe the meanings of expressions from the languages. Source: Wikipedia
Questions tagged [denotational-semantics]
16 questions
925
votes
6 answers
What part of Hindley-Milner do you not understand?
I swear there used to be a T-shirt for sale featuring the immortal words:
What part of
do you not understand?
In my case, the answer would be... all of it!
In particular, I often see notation like this in Haskell papers, but I have no clue what…
MathematicalOrchid
- 61,854
- 19
- 123
- 220
26
votes
1 answer
The concept of Bottom in Haskell
Bottom in Haskell described here is said to be any computation that have errors, is unterminated, or involves infinite loop, is of any type... is this specific to Haskell? We know in Lattice theory, there is also a notion of Bottom there.....and…
user618815
12
votes
1 answer
What goes into writing a denotational semantics mapping function?
I am a bit confused on the concept of denotational semantics. As I understand, denotational semantics are supposed to describe how functions and expressions work in a particular programming language. What exactly is the proper form used to describe…
tbogatchev
- 1,531
- 3
- 14
- 21
8
votes
1 answer
Does Haskell's 'evaluate' reduce to normal or WHNF?
I understand (I think) that Haskell's seq, will (generally) reduce its first argument to WHNF, and see this behavior as expected in GHCi:
λ> let x = (trace "foo" Foo (trace "bar" Bar 100)) in seq x 0
foo
0
However, though the documentation for…
orome
- 45,163
- 57
- 202
- 418
7
votes
1 answer
Termination checking in functional programs
Are there functional languages that can specify, in the typechecker, whether or not a certain computation is guaranteed to terminate? Alternatively, can you do this in just Haskell?
Regarding Haskell, in this answer the poster says that
The usual…
Dan
- 12,409
- 3
- 50
- 87
4
votes
1 answer
Writing a haskell program for computing denotational semantics of an imperative programming language
I am trying to write a program in Haskell to compute the denotational semantics of an imperative language program with integer variables, 1-dimensional (integer) arrays and functions. The function I am starting with is of the type:
progsem ::…
Justin B
- 110
- 1
- 8
3
votes
1 answer
Natural map derivation algorithm
This Reddit post by Edward Kmett provides a constructive definition of a natural map, the one from the free theorem for fmap (which I read in yet another Edward Kmett's post):
For given f, g, h and k, such that f . g = h . k: $map f . fmap g = fmap…
Zhiltsoff Igor
- 1,812
- 8
- 24
3
votes
2 answers
What is denotational semantics?
I am looking for an accurate and understandable definition. The ones I have found differ from each other:
From a book on functional reactive programming
Denotational semantics is a mathematical expression of the
formal meaning of a programming…
XYseven
- 475
- 1
- 4
- 11
2
votes
1 answer
Why are functions names classified as L-value expressions?
According to Christopher Strachey’s paper The Varieties of Programming Language on denotational semantics, in any programming languages names can be bound to bindable values, which is represented by the function environment: Id -> D, where Id are…
Géry Ogam
- 6,336
- 4
- 38
- 67
2
votes
1 answer
Free theorem for fmap
Consider the following wrapper:
newtype F a = Wrap { unwrap :: Int }
I want to disprove (as an exercise to wrap my head around this interesting post) that there’s a legitimate Functor F instance which allows us to apply functions of Int -> Int type…
Zhiltsoff Igor
- 1,812
- 8
- 24
2
votes
1 answer
In what sense is one function "less defined" than another?
What I mean is that, from definition:
fix f is the least fixed point of the function f
In other words:
the least defined x such that f x = x.
The least defined value of any nullary type is undefined. There is some ambiguity here still as…
Ignat Insarov
- 4,660
- 18
- 37
1
vote
1 answer
Denotational semantics, proving that fixed point iteration results in the least fixed point
I'm working through the Haskell wikibook section on denotational semantics and I'm kind of stuck on this exercise:
Prove that the fixed point obtained by fixed point iteration starting
with is also the least one, that it is smaller than any…
Sam van Herwaarden
- 2,321
- 14
- 27
1
vote
1 answer
How do I denote this syntax's semantics?
I am writing a language specification, and I need the following rudimentary question resolved. Suppose I have the (admittedly contrived) abstract syntax:
::= |
::= 1 | 2 | 3
::= 4 | 5 | 6
What does the denotational semantics…
Dan Barowy
- 2,270
- 24
- 35
0
votes
1 answer
How to add function and procedure abstractions denotational semantics using haskell?
I want write a haskell program to implement a simple imperative language based on its denotational semantics.
I use GHCi, version 8.4.2 on windows.
I encountered some issue when implementing function and procedure abstraction described below.
let me…
Charlie Huang
- 13
- 2
0
votes
0 answers
Formal verification using denotational semantics?
This might go to cs or cstheory stack exchange, but I have seen the most questions tagged with formal-verification here.
Is there extensive literature on using denotational semantics for program verification?
With a quick search I have…
Gergely
- 6,879
- 6
- 25
- 35