Questions tagged [pl.programming-languages]
Programming languages, in particular, focussing on their semantics.
378
questions
49
votes
7
answers
8k
views
What constitutes denotational semantics?
On a different thread, Andrej Bauer defined denotational semantics as:
the meaning of a program is a function of the meanings of its parts.
What bothers me about this definition is that it doesn't ...
- 135
2
votes
0
answers
82
views
When is an upper bound on the longest irreducible program outputting something computable?
This is a repost of this mathoverflow question.
Given some way to to encode programs to strings with a finite alphabet, which we assume has a computable translation to/from Turing machines, a program ...
- 567
7
votes
0
answers
118
views
Are there any programming languages based on the method of analytic tableaux, aside from Fitting's Proflog?
The method of analytic tableaux [0] describes a process by which logical formulae, particularly of first order logic, can be determined to be valid or invalid. From the Wikipedia entry:
A tableau ...
- 109
5
votes
0
answers
177
views
Can a positive elementary inductive definition refer to its own stage comparison relation?
Moschovakis' stage comparison theorem says that the stage comparison relation associated with any positive elementary induction is itself definable by (another) positive elementary induction. But what ...
- 541
1
vote
0
answers
82
views
How to Classify Memory Access Pattern by LLVM or Other Tools?
I am currently encountering issues with using LLVM. Here is my specific problem:
I want to study the memory access patterns of applications that are suitable for mapping onto a Spatial Accelerator, ...
- 21.8k
5
votes
5
answers
4k
views
Is there such a thing as a state-based programming language?
As anyone knows who has read Alan Turing's paper describing the Turing Machine (On Computable Numbers, With an Application to the Entscheidungsproblem), the syntax he uses is vastly different from ...
- 18.2k
8
votes
1
answer
369
views
In logic programming, what would a language with second-order model theory gain?
HiLog is described as a logic programming language with higher-order syntax, but first-order model theory.
For example, it allows you to define a map over lists:
...
- 259
1
vote
0
answers
90
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:
...
- 10.9k
2
votes
2
answers
344
views
A few questions about ISWIM
I recently read Landin's paper "The Next 700 Programming Languages". But I was a bit confused by ISWIM. In particular, are functions first-class objects in ISWIM? It seems not because every ...
- 161
10
votes
4
answers
7k
views
Difference between Strict Consistency and Sequential Consistency
I understand strict and sequential consistency independently fairly well.
Strict C basically enforces the actual order in which the instructions ran on the global clock.
Sequential Consistency ...
- 101
4
votes
1
answer
172
views
Is there a high level (functional) language compiling to Mixed Integer Linear Programming problems?
Many different kinds of optimization problems can be expressed as Mixed Integer Linear Programming (MILP). The translation is usually very direct, and one has to encode invariants as constraints in a ...
- 12.3k
4
votes
0
answers
93
views
Description of the CPS transformation for the typed lambda-calculus
Is there somewhere a precise but hopefully readable account of how the CPS (=continuation-passing-style) transformation applies to the typed lambda-calculus? (Say, simply-typed with product and sum ...
- 851
-1
votes
1
answer
86
views
Generating grammar from a string
Given a string generated with a valid grammar, how can I find list of all the valid grammar for that particular string?
Problem statement - I'm trying to build a code base scanner, and I'd like to ...
- 11.5k
7
votes
1
answer
208
views
Can you regain the Church-Rosser property in languages with continuations?
I'm aware that if you naively add continuations to a language, the Church-Rosser property no longer holds. For example, suppose we have some variant of the STLC with basic arithmetic and integer types....
- 11.5k
3
votes
1
answer
78
views
Is Linear Evaluation Parametric?
Parametric functions satisfy free theorems which state that they take related arguments to related results. This is formalized by the notion of parametric transformation introduced in section 5 of ...
- 1,021
7
votes
2
answers
342
views
Efficiently ordering typed programs
Sometimes it is useful to enumerate in increasing order
programs that have a given type. A
simple example is test
generation for compilers: we want to test a new optimising phase and
are ...
- 11.5k
0
votes
1
answer
130
views
Formal differences between emulation and simulation?
Recently this question came up, and I've been unable to find a concrete answer.
When I was reading this paper on CRDTs, I was a little perplexed by the notion of emulation here in theorems 3.1 and 3.2....
CommunityBot
- 1
1
vote
1
answer
219
views
Is data structure necessarily a functor?
The justification of my conjecture is that (seemly) any data structure can have a mapper that applies a given function $f$ to each element of the structure. A data structure in the end is a container ...
- 29.4k
14
votes
4
answers
2k
views
Where is the model theory in programming language theory?
I have a background in mathematical logic and am trying to learn some programming language theory. In the syntax of, say, first-order logic, one of the first distinctions you learn about is between ...
- 851
9
votes
3
answers
338
views
Resumption-based IO systems?
I've been playing around with resumptions lately, mostly from Abramsky's classic paper Retracing Some Paths in Process Algebra. They are quite slick (basically solutions to the domain equation $R = I \...
-1
votes
1
answer
102
views
Typing rule for corresponding `val` and `let` bindings
$\newcommand{\clet}{\texttt{let }}
\newcommand{\cval}{\texttt{val }}
\newcommand{\cin}{\texttt{ in }}
$I have the syntax for a programming language containing both let-bindings of the form $\clet x = ...
- 18.2k
7
votes
2
answers
6k
views
What's the difference between an invariant and an "inductive" invariant?
I would like to understand this with an example. Also, are there other kinds of invariants related to these?
Thanks!
- 191
5
votes
2
answers
366
views
Lambda-calculus: Beta-equivalent terms have the same type
In the simply-typed lambda calculus, how do you prove that: If two terms are beta-equivalent, then they have the same type?
My guess is that I should use the subject reduction, and maybe the ...
- 5,598
1
vote
0
answers
94
views
Is it possible to define beta reduction for PHOAS?
I'm using Parametric Higher-Order Abstract Syntax (PHOAS) as a representation for untyped lambda calculus in OCaml:
...
- 105
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 ...
- 103
13
votes
4
answers
836
views
Can any program be implemented mechanically?
Is it possible to build a single purpose (non Turing complete) mechanical implementation of say, Microsoft Word? Is it possible to implement such things as iterators, first-order functions, the whole ...
- 95
6
votes
0
answers
115
views
List Functions That Don't Depend on Length
Intuitively, a polymorphic function of type $f : \forall a. [a] \to [a]$ cannot inspect the type of its elements. This intuition can be captured formally using either natural transformations or ...
- 93
9
votes
1
answer
172
views
What is known about reduction by "$P_1$ interprets $P_2$" for generalized programming languages?
Inspired by this answer, let's say that a programming language is given by the data $L=(P,ev)$ where $P$ (the set of "valid programs") is a computable subset of $\Sigma^*$ and $ev$ (the "evaluator") ...
- 851
8
votes
0
answers
135
views
Does Bellantoni-Cook safe recursion (or any other implicit characterization of P) admit Kleene's second recursion theorem?
Abstractly, by a programming language that operates on binary strings I mean a set $P$ of programs along with a semantics relation $[p](x) = y$, ``the program $p$ on string $x$ halts with output $y$.&...
- 851
7
votes
1
answer
527
views
The precise definition of Normalization By Evaluation?
The Wikipedia article suggests that NbE is a technique for obtaining "the normal form of terms" by translating the object language into abstractions of the meta (host) language:
The ...
- 32.8k
2
votes
1
answer
94
views
Nominal Tree Languages i.e. with Binders and Infinite Symbols?
I'm wondering if there has been any research done into automata that accept languages of trees that can bind arbitrary variables, and are considered equal under alpha equivalence.
I've found so far:
...
1
vote
0
answers
100
views
Alternative notions of bisimulation
Suppose $(S, \Lambda, \rightarrow)$ is a labeled transition system. A bisimulation is a relation $R \subseteq S \times S$ s.t. $\forall \alpha \in \Lambda$ and $\forall p, q \in S$ with $R(p,q)$,
$\...
- 11
1
vote
1
answer
117
views
Extension of primitive recursion, that is as powerful as System-T
I know that System-T restricted to first-order types is exactly as powerful as primitive recursive functions, because I proved it in Agda.
I asked myself, if there is a extension of primitive ...
- 14k
1
vote
0
answers
81
views
Decision vs search problem specification
Let us suppose we have a sort function.
One way of specifying it is to say that a sort function is any function where if the input/output are vectors $I, O$, then $O_i \leq O_j \forall i < j$ and ...
- 1,311
7
votes
1
answer
261
views
Has anyone studied "polynomially compact" metric spaces?
A subspace $S$ of a metric space $A$ is compact if it is complete and totally bounded. Here, complete means that every Cauchy sequence in $S$ has a limit also in $S$. For $S$ to be totally bounded, ...
- 359
0
votes
0
answers
66
views
Has there already been research done on how data(e.g. runtime) can improve the development environment of a language?
tl;dr; I am being offered a graduate thesis about how to use data about a languages runtime/static analysis of dependencies etc. and feed it back into the development process. And my question is: Has ...
- 125
4
votes
1
answer
153
views
Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?
This question extends my inquiry from a previous post [0].
Dan Willard's Self-Justifying Axiom Systems/Self-Verifying Theories [1] and Brown and Palsberg's self-interpreter for F-Omega [2] both employ ...
- 1,021
2
votes
0
answers
101
views
Is there a relationship between Brown and Palsberg's Self-Interpreter for F-Omega and Lawvere's Fixed Point Theorem?
Brown and Palsberg [0] demonstrated an self-interpreter for F-Omega. To do so, they perform "a careful analysis of the classical theorem [of the impossibility of self-interpretation by total ...
- 109
3
votes
1
answer
433
views
Similarities and differences between Pie and popular languages with dependent types
The book The Little Typer explains dependent types using a toy language called Pie (https://github.com/the-little-typer/pie).
How similar is Pie to the popular languages with dependent types: Coq, ...
0
votes
0
answers
119
views
Programming languages with constraints on values of variables?
Hi Theoretical Computer Science Stack Exchange,
I have been wondering if there are programming languages where one can have constraints on values variables can have?
Have such approach been used in ...
2
votes
1
answer
192
views
Intuitive way to handle variable binding
Suppose we have an algebraic datatype parameterised by a type variable name, e.g.
...
- 29.4k
8
votes
3
answers
771
views
What's the logical counterpart to jumps with arguments on CPS terms?
It's well known that the CPS (continuation-passing style) translation often employed in compilers corresponds to double negation translation under the Curry-Howard isomorphism. Though often the target ...
7
votes
0
answers
139
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. ...
- 29.4k
4
votes
1
answer
199
views
Is Barbara Liskov's claim that CLU was the first implemented language to provide linguistic support for data abstraction accurate?
According to this paper by Barbara Liskov, CLU was "The first implemented programming language to provide direct linguistic support for data abstraction".
She then defines "data ...
- 186
4
votes
0
answers
57
views
Coinduction principle for smash products of pointed cpos
In "Relational Properties of Domains", Pitts gives a coinduction principle for pointed cpos (cppos). In corollary 6.13 (below), he specializes it to cppos constructed as fixed points of cppo-...
- 141
6
votes
3
answers
2k
views
How does type theory change how one thinks about programming?
I have been dabbling in HoTT and I am convinced that dependent type theory is much more suitable than set theory for proof assistants.
Now, this made me wonder - how fundamental is Type Theory ...
- 271
0
votes
0
answers
181
views
Is BigInteger-based Brainfuck Turing Complete?
All of the proofs of Turing-Completeness I've found for Brainfuck rely on its cells being fixed-width integers that wrap around upon over/underflow. The "parent language" P'' on which ...
- 25
2
votes
0
answers
75
views
Reference request: characterisation of simultaneous substitution
For simply typed λ-calculus, a simultaneous substitution from $\Gamma$ to $\Delta$ is concretely a type-preserving map from variables in $\Delta$ to terms in $\Gamma$. See, for example, Programming ...
- 121
3
votes
0
answers
179
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 ...
- 851
10
votes
0
answers
235
views
What is the "standard" lambda-calculus model for bicartesian closed categories?
(I'm familiar with the lambda-calculus, less so with its categorical models.)
It is well-known that cartesian-closed categories are in tight correspondence to the simply-typed lambda-calculus with ...
- 2,040