2022 Developer Survey is open! Take survey.

# Tag Info

Accepted

• 8,178
Accepted

### Break keyword outside a loop is syntax error or semantic error?

Both work, so how you do it is up to you. But there are a couple of reasons to consider doing it during a post-parse analysis: While it is certainly possible to define two different types of ...
• 11k
Accepted

Note: parameter passing by xxx is sometimes called "pass by xxx" and sometimes "call by xxx". I will use both expressions indifferently. Parameter passing by value-result consists in passing by ...
• 19.1k

### Which fixpoint is Haskell list type?

It's the greatest fixed point, or the final coalgebra, depending on how you set things up. In Haskell it is impossible to define the datatype of finite lists because Haskell does not have inductive ...
• 28.1k
Accepted

### What's the difference between a calculus and a programming language?

The meaning of the words is not fixed, but I can give you my interpretation. A calculus is something that we calculate with in the sense of juggling equations (think manipulation of Taylor series or ...
• 28.1k

### What are the axioms, inference rules, and (formal) semantics of lambda calculus?

First of all, note that the notion of a formal system is an informal notion and there is no general (or generally accepted), formal definition of what a formal system is. In my opinion, the Wikipedia ...
Accepted

### Is reference counting GC vs. tracing GC a language property or an implementation property?

Swift guarantees that once the last reference to an object is dropped the object is deinitialized, and the deinit code is immediately run. Obtaining this kind of ...
• 14.1k

### Why do some authors not include summation in the $\pi$-Calculus?

To answer this question, it's best to reflect on the meaning of sums in process calculi. Essentially sums express a lack of knowledge. The process $P + Q$ means something along the lines of "either $P$...
• 8,178
Accepted

### What formal representation is commonly used to describe compiler optimizations?

There are many compilers, which compile widely different kinds of languages which serve widely different purposes. For example, a database language will have very different optimizations than an array-...
• 7,744
Accepted

### Lambda Calculus: How do evaluation contexts "work"

The subtlety lies in where the distinction between language and metalanguage is made. As René Magritte put it: $(\lambda f. \lambda x. f x) ((\lambda y.y) (\lambda z.z)) (\lambda w.w)$ is a lambda-...

### Does a logical system have semantics?

Semantics of a logic describe how to compute the truth value of an expression, possibly given some interpretation. For example, one rule would say that an expression $\varphi \land \psi$ is true iff ...
• 269k

### What is a predicate transformer?

The predicate transformer is just a formalization of the idea that you can produce a precondition given a program and its postcondition. For example, given a program ...
• 199

### When would one use equational dynamics?

What you call "equational dynamics" is not actually an operational semantics, it's an equational theory. As you note, equations by themselves do not tell us how to run programs. However, they are ...
• 28.1k
Accepted

### Programming language semantics prototyping tool

Although there are frameworks created specifically for the purpose of prototyping programming languages (including their semantics, type systems, evaluation, as well as checking properties about them),...
• 540
Accepted

### What does it mean to "strengthen the precondition and weaken the postcondition" in Hoare logic?

Condition $A$ is stronger than condition $B$ if $A$ implies $B$. That is, if $B$ holds in all situations in which $A$ holds. Conversely, if $A$ is stronger than $B$, ...
• 80.1k

### Formal model of execution for Java (or general imperative language)

There is an (operational) semantics for Java 1.4 formulated in the $\mathbb{K}$ framework. Associated to this framework is a proof system called Matching Logic. While that page describes a prototype ...
• 11.8k

### Does a logical system have semantics?

The answer to your literal question, "Does a logical system have semantics?" is "Obviously, yes. The definition you quoted says so!" So I figure that isn't what you're actually asking. I think the ...
• 80.1k
Accepted

### Are syntax and semantic just 2 structures such that one is a model of the other?

I am afraid the phrasing of the question misled me (though I did know better) in first seeing model theory as applying to any two arbitrary mathematical structures, and being the study of ...
• 19.1k

### What is this fraction-like "discrete mathematics"–style notation used for formal rules?

Here is a very informal explanation that might help people unfamiliar with formal notations to get a foot in the door. It does not replace a formal definition! The Ap is the state of your system or ...
• 171
Accepted

### Formal model of execution for Java (or general imperative language)

Featherweight Java is quite highly regarded in the PL community. But if that doesn't suit your needs, here's a general approach to modelling: Formalize your language's AST into expressions and ...
• 29.1k
Accepted

### What is meant by a full abstract model of a lambda-calculus like language?

In denotational semantics, you want to be able to map each of your language terms to some object in your semantic domain or model. Now, it cannot be any arbitrary domain/model as you like, but, ...
• 619

### Is type-checking "syntactic" or "semantic"?

Although I personally would describe type analysis as semantic, this question seems to start with the assumption that there is a clear, formally-definable dividing line between "syntax" and "semantics"...
• 11k

### denotional semantic for while - fixed points

Your proposed alternate definition is no good. It tries to define $[[\text{while b do S}]]$ in terms of $[[\text{while b do S}]]$. That's a circular definition: you can't define something in terms ...
• 140k

### Typing dependent pattern matching

In general matching with dependent types can be quite subtle! You'll note that in the Coq documentation that the extended pattern-matching syntax is ...
• 7,744

### Why injection into sum type apparently leads to ambiguity?

I think the key point here is $\sigma$, $\tau$ and $\phi$ are type variables, and not specific types. So, what the typing rule for $\operatorname{inl}$ says is that $\operatorname{inl} M$ is of type \$\...
• 1,846
Accepted

### How to express modalities in lambda calculus - are some extensions required?

Are extensions required? Not really. You can take an axiomatic description of a modal logic and simply provide a "primitive" lambda term for each. The modal operators would become type constructors. ...
• 11.8k
Accepted

### What's the difference between: operational, denotational and axiomatic semantics?

I think your examples show you do somehow understand the basic points of the several styles of semantics. Still, note that the whole point of having a semantics of a programming language is to have a ...
• 14.1k