Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [semantics]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
1 vote
0 answers
84 views

Abstract domain monad

I was reading old lecture from a CS course at Cornel and I have some doubts about the following at 2.4 It defines how to transform domains between each other via a Galois Insertion, more formally: ...
Alecs's user avatar
  • 11
0 votes
1 answer
73 views

Is there such a thing as "transformational semantics"?

The Wikipedia article about programming language semantics distinguishes three major approaches to semantics: denotational, operational, and axiomatic. What is the approach called when the meaning of ...
Evan Aad's user avatar
  • 354
1 vote
0 answers
141 views

Operational semantics and denotational semantics and describing the behaviour and structure of programs

I was under the impression that operational semantics describes the behaviour of a program (so it includes the implementation details / the implementation matters), whereas denotational semantics ...
The Pointer's user avatar
0 votes
0 answers
31 views

Which family of bicartesian closed functors can define the semantics of simply typed lambda calculus with products and sums

Given any bicartesian closed category $\mathbf{C}$, any natural number $n \geq 0$, and any vector $\boldsymbol{A} \in \mathbf{C}^n$ with $n$ objects $A_1, A_2, … A_n \in \mathbf{C}$, how can I define ...
Johan Thiborg-Ericson's user avatar
1 vote
0 answers
83 views

Do game semantics for logic have Curry-Howard-like correspondence with game semantics for programming languages?

Both for logic and PLs do have notion of game semantics. Both are defined by two-player dialogue game, but players are different. In first case it is game between Verifyer and Falsifyer and in second ...
uhbif19's user avatar
  • 315
2 votes
0 answers
52 views

Formal semantics of a simple object oriented language without inheritance but with self-referential objects

Would you please point me to some papers or textbooks that describe rigorously a formal semantics/computational model of a simple object-oriented language? The language needs not accommodate ...
Evan Aad's user avatar
  • 354
3 votes
1 answer
50 views

Equivalence of finitary and infinitary semantics of concurrent programs

The following claim is stated on p. 155 of Manna and Pnueli's The Temporal Logic of Reactive and Concurrent Systems: Specification. Let $P_1$ and $P_2$ be two finitely branching transition systems ...
Evan Aad's user avatar
  • 354
0 votes
1 answer
70 views

Proper terminology for input, parameter or variable fixing. Refinement? Projection? Fixation? Partial valuation?

I contemplate writing a paper on automating fixing some inputs/parameters to specific values in a kind of workflow/pipeline definition language/system and looking for best terminology. English is not ...
Serge's user avatar
  • 111
3 votes
1 answer
92 views

Does ${\bf CPO}$ have $\omega$-colimits?

Does the category ${\bf CPO}$ have $\omega$-colimits? By ${\bf CPO}$ I mean the category that has as objects the $\omega$-complete pointed partial orders and as arrows $\omega$-continuous functions.
LaR's user avatar
  • 335
3 votes
1 answer
139 views

Terminal object in the category of embeddings

Let ${\bf CPO}$ be the category of $\omega$-complete partial orders and $\omega$-continuous functions. Let ${\bf CPO}^{E}$ be the category of embeddings of ${\bf CPO}$. Does ${\bf CPO}^{E}$ have a ...
LaR's user avatar
  • 335
4 votes
1 answer
145 views

"Operations" in category theory that are not defined for arrows

Functors in category theory are defined for both objects and arrows. Depending on how they treat arrows, functors are characterized as either covariant or contravariant. Some "operations" ...
LaR's user avatar
  • 335
0 votes
1 answer
59 views

Are there logical devices similar to "existential variables" or "blank nodes" of Semantic Web?

In Semantic Web, alongside permanent names of things also "temporary names" named "existential variables" or "blank nodes" denoted as "_:label" are used. All ...
Ioachim Drugus's user avatar
4 votes
1 answer
243 views

Semantics of logic/relational programming languages

I'm working on some vague ideas about a logic/relational programming language based on the linear lambda calculus and having trouble coming up with some appropriate semantics. If anything the language ...
Ms. Molly Stewart-Gallus's user avatar
7 votes
0 answers
140 views

Are the non-lazy / non-weak semantics of the $\lambda$-calculus related to weak evaluation?

Vague question The most common semantics of the call-by-name $\lambda$-calculus (Hyland/Wadsworth’s observational equivalence $\approx_\text{HNF}$ and Morris’s observational equivalence $\approx_\text{...
xavierm02's user avatar
  • 556
7 votes
0 answers
138 views

Halting problem for finitary PCF

Is the halting problem decidable for finitary PCF? By "halting problem" I mean the problem of deciding whether a closed PCF term evaluates to bottom under the denotational semantics of PCF. ...
PaR's user avatar
  • 71
8 votes
2 answers
558 views

What's the categorical semantics of definitional equality?

The categorical semantics of a dependent type theory is normally described as a CwA/CwF/CompCat/etc. and in these models, we can talk about propositional equality by interpreting an 'identity type'. ...
ice1000's user avatar
  • 965
3 votes
0 answers
171 views

syntax and semantics for transfinite algorithms

Let's say I wanted to informally describe a very simple algorithm for searching through an (undirected) finite connected graph $G = (V,E)$. I could define, for each natural number $n$, a set $S_n$ and ...
Siddharth's user avatar
  • 851
4 votes
2 answers
292 views

Density of semantics in syntax

Let $L$ be a programming language, and $\cong$ a notion of equality of $L$-programs (in general $\cong$ will be undecidable). Let $syntax(n)$ be the number of $L$-programs of size $n$ (for some ...
Martin Berger's user avatar
1 vote
1 answer
224 views

What relations and differences are between formal semantics for linguistics and for programming languages?

I browsed the table of content of Cann's Formal Semantics, which reminds me of the things that I saw in programming language books. Cann's book is for linguistics, and am I right that it is helpful ...
Tim's user avatar
  • 639
-1 votes
1 answer
84 views

Al-Mubaid's Similarity Measure for Ontological Concepts

Al-Mubaid et al. proposed a semantic similarity measure in their research paper [1]. They see ontologies as connected graphs but refer to clusters within ontology graphs without ever defining what ...
AzLimbiate's user avatar
4 votes
0 answers
132 views

Origin of simulation relations for compiler correctness

Leroy uses simulation relations as a means of showing compiler correctness; the basic idea is that a simulation relation is an asymmetric binary relation between states in two different small step ...
denotational's user avatar
-2 votes
1 answer
74 views

Is there an official/academic name for the "current value" in a loop? [closed]

This is a question about semantics/vocabulary. I don't like saying "the current value you are looping over/on". I'm wondering if there is a better term.
Niko Bellic's user avatar
7 votes
1 answer
138 views

Semantic read-back of sharing graphs

A "sharing graph" is a representation of a $\lambda$-term that modifies an abstract syntax tree by adding edges connecting each variable use to the place where that variable is bound. They are used ...
Mike Shulman's user avatar
9 votes
3 answers
506 views

Can Non-termination be considered an algebraic effect?

Non-termination is sometimes considered an effect. I have been reading about algebraic effect systems (What is algebraic about algebraic effects and handlers?), and I suspect non-termination (like ...
user833970's user avatar
5 votes
1 answer
169 views

Is there a notion of "inevitable reduction?"

I was just working on a semantics paper and realized I needed a notion of inevitable reduction. I came up with this definition: Let $\rightarrow$ be a binary relation. We say that $a$ inevitably ...
James Koppel's user avatar
6 votes
2 answers
129 views

Formal semantics of tactics

Tactics are supposed to represent inference rules in a system, and it might seem unnecessary at first to formalize the semantics of tactics; nevertheless, modern theorem provers can have pretty ...
xrq's user avatar
  • 1,175
4 votes
2 answers
689 views

What does the category of RDF models look like in Institution Theory?

The Question in short Here is the question in its pure form. Details of my reasoning can be found below. The RDF1.1 spec semantics defines a model to consist of a set IR of objects and IP of ...
Henry Story's user avatar
7 votes
4 answers
7k views

Difference between syntax and semantic error in programming languages

When compilers generate errors for a specific programming language, there's distinction between syntax & semantic errors. E.g. ) + f 3 has ill-formed syntax, ...
Rui Liu's user avatar
  • 181
5 votes
1 answer
229 views

What is a 'free model'?

I was reading this paper on effect handlers and got hung up on the phrase 'free model'. In context: [...] From an algebraic point of view, the $x_e$ provide a model for the theory of ...
user's user avatar
  • 615
21 votes
2 answers
2k views

Has the semantics of TeX (as a programming language) ever been formalized?

It seems to me that the macro language employed by $\TeX$ can maybe be seen as some kind of term rewriting system or some kind of programming language with call-by-name scoping. Even modern ...
Nicola Gigante's user avatar
5 votes
0 answers
96 views

Which computational models support bigotous programs?

A bigotous program is a program which decides if its input is semantically equivalent to itself. Of course, this is impossible in a Turing complete language due to Rice's theorem. In fact, its pretty ...
Christopher King's user avatar
3 votes
2 answers
193 views

Why is the multi-step reduction of semantics reflexive?

I was reading Programming Languages and Lambda Calculi, which defines the multi-step reduction to be the reflexive-transitive closure of the one-step reduction. (Page 15, $\twoheadrightarrow_r$ is the ...
wlnirvana's user avatar
  • 173
2 votes
0 answers
121 views

Applications of the monoidal closed structure in LTL?

A simple model of temporal logic is via time-indexed truth functions. This lets us model the Boolean connectives, as well as the next-step operator and modal always operator: $$ \begin{array}{lclll} ...
Neel Krishnaswami's user avatar
2 votes
0 answers
176 views

Is there is an intuitive explanation why call-by-name PCF is less expressive than both call-by-value PCF and lazy PCF?

J.C. Mitchell cites in his "Expressive power of programming languages" the result in Riecke's "Fully abstract translations between functional languages" about the call-by-value, call-by-name and lazy ...
Akram El-Korashy's user avatar
6 votes
1 answer
356 views

Standard reference for basic model theory definitions

I am trying to give a formal presentation of the model-theoretical semantics of a language and I am a bit lost in the terminology. In particular, could somebody clarify the exact definitions of model-...
AnaK's user avatar
  • 203
1 vote
1 answer
154 views

Observational Equivalence of open terms in PCF

The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms. Lets consider the simple case where the terms ...
Adribar's user avatar
  • 31
3 votes
1 answer
186 views

In what fields does a knowledge of formal semantics prove useful?

(If this is better for programmers SE, let me know, but I imagined you guys would have more thorough answers) I'm a mathematics major, but I have a pretty deep interest in CS (especially in compiler ...
galois's user avatar
  • 131
8 votes
2 answers
489 views

Precise definition of syntatic categories / syntatic domains in abstract syntax

I have read the introductory parts of a couple of books on programming language semantics (Gordon, Winskel, Nielson & Nielson, Allison, Stump, Schmidt), and while I do understand what they mean by ...
josh's user avatar
  • 235
1 vote
1 answer
148 views

How to specify and verify Horn clauses (logic programming programs)? Semantics of Horn clauses

There are lot of applications of Horn clauses (notable examples include use of rules in cognitive architectures and knowledge bases, as well as use of rules in business rules programs). Are there ...
TomR's user avatar
  • 409
10 votes
2 answers
750 views

What's the difference between reduction strategies and evaluation strategies?

From the evaluation strategy article on Wikipedia: The notion of reduction strategy in lambda calculus is similar but distinct. From the reduction strategy article on Wikipedia: It is similar ...
Clément's user avatar
  • 281
0 votes
0 answers
245 views

How do we contribute to the lexicon of computer science?

What's the best way to contribute to the lexicon of computer science? There is an obvious organic nature to the naming of things in most sciences. The name of the discoverer is inherited or bestowed, ...
Christian Davis's user avatar
1 vote
1 answer
1k views

What is the relation/difference between axiomatic and denotational semantics one one side, and the data flow analysis(DFA) on the other sied?

I am supposed to write a small paper about DFA in OOP for a CS class in theory. But I am required to connect that (DFA) to axiomatic and denotational semantics! I read few resources about axiomatic/...
salouri's user avatar
  • 113
1 vote
1 answer
175 views

Name a set of program variables

I am interested in the set of the variables that satisfy the following properties. I would like to find a proper name for them. We assume that a program $\phi$ has a set of variables $v_0, \ldots, ...
SoftTimur's user avatar
8 votes
2 answers
441 views

Categorical semantics for non-monotonic logics?

Are there any categorical semantics for non-monotonic logics? It appears that the simple answer to this is "No" since the obvious notion of composition fails for any model of a non-monotonic logic. ...
David Boshton's user avatar
3 votes
2 answers
282 views

What requirements should a denotational semantics for a programming language satisfy to be correct?

We have a programming language and its denotational semantic, like Tony Hoare's CSP with its syntax and denotational semantic e.g. stable failure and UTP. We want to extend the language (its ...
zhuang's user avatar
  • 31
6 votes
1 answer
2k views

How can I prove formally semantic equivalence of programming languages?

I would like to compare two languages which are from different programming paradigms. Both languages are object oriented languages, but one of them a multiparadigm language because it supports ...
bitli's user avatar
  • 163
10 votes
1 answer
226 views

Program Minimization

Circuit Minimization is the problem to minimize the size of a given circuit. Is there anything similar for general programs? In particular my question is - Do there exist algorithms to minimize the ...
Opt's user avatar
  • 1,311
2 votes
2 answers
307 views

Tool for specifying operational semantics for given formally specified programming language

I am trying to translate code from one programming language into another (to be specific - from RuleML to Drools, but other pairs can be expected as well) and it would be nice to know - whether there ...
TomR's user avatar
  • 409
11 votes
1 answer
630 views

What exactly does "semantically observable" side-effect mean?

I have question regarding pure functions. According to the Wikipedia page one of the requisites for a pure function is : Evaluation of the result does not cause any semantically observable side ...
Henrik Sommerland's user avatar
3 votes
2 answers
311 views

Difference between abstract machines and calculi

So, first of all: I'm not sure how to tag this question. Feel free to tag it differently. I recently started reading up on CHAMs, which can express different process calculi. Slightly confused, I go ...
user's user avatar
  • 615