Questions tagged [semantics]
The semantics tag has no usage guidance.
80
questions
0
votes
0
answers
29
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 ...
1
vote
0
answers
68
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 ...
- 295
2
votes
0
answers
51
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 ...
- 354
3
votes
1
answer
49
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 ...
- 354
0
votes
1
answer
68
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 ...
- 111
3
votes
1
answer
88
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.
- 193
3
votes
1
answer
133
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 ...
- 193
4
votes
1
answer
142
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" ...
- 193
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 ...
- 101
4
votes
1
answer
231
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 ...
7
votes
0
answers
137
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{...
- 556
7
votes
0
answers
135
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. ...
- 71
8
votes
2
answers
510
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'. ...
- 965
3
votes
0
answers
168
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 ...
- 803
4
votes
2
answers
291
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 ...
- 11.4k
1
vote
1
answer
205
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 ...
- 639
-1
votes
1
answer
82
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 ...
- 11
4
votes
0
answers
126
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 ...
- 41
-2
votes
1
answer
73
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.
- 99
7
votes
1
answer
132
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 ...
- 675
9
votes
3
answers
468
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 ...
- 546
5
votes
1
answer
168
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 ...
- 455
6
votes
2
answers
125
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 ...
- 1,175
4
votes
2
answers
672
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 ...
- 575
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, ...
- 181
5
votes
1
answer
212
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 ...
- 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 ...
- 1,588
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 ...
- 471
3
votes
2
answers
189
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 ...
- 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}
...
- 32.4k
2
votes
0
answers
166
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 ...
6
votes
1
answer
351
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-...
- 203
1
vote
1
answer
151
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 ...
- 31
3
votes
1
answer
185
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 ...
- 131
8
votes
2
answers
477
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 ...
- 235
1
vote
1
answer
147
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 ...
- 409
10
votes
2
answers
713
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 ...
- 281
0
votes
0
answers
243
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, ...
- 101
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/...
- 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, ...
- 73
8
votes
2
answers
423
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. ...
- 191
3
votes
2
answers
276
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 ...
- 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 ...
- 163
10
votes
1
answer
224
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 ...
- 1,311
2
votes
2
answers
294
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 ...
- 409
11
votes
1
answer
618
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 ...
3
votes
2
answers
309
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 ...
- 615
18
votes
2
answers
2k
views
Full Completeness vs Full Abstraction of a program translation
Compiler verification efforts often come down to proving the compiler fully abstract: that it preserves and reflects (contextual) equivalences.
Instead of providing full abstraction proofs, some ...
- 485
5
votes
0
answers
236
views
What's the connection between these two categories of games and innocent strategies?
Lately I've been reading a lot about game semantics and in particular the problem of PCF's full abstraction.
I'm trying to understand how the definition from this article relates to the one found in ...
- 151
0
votes
1
answer
136
views
How would you define a set of 'fundamental operations' over an object? [closed]
I'm writing an implementation for a common array structure.
As you would find already familiar, an array is an ordered data structure that you can transform with different (hopefully self-explained) ...
- 125