Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

Filter by
Sorted by
Tagged with
3 votes
1 answer
149 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 ...
Turion's user avatar
  • 616
4 votes
0 answers
64 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 ...
Gro-Tsen's user avatar
  • 841
5 votes
0 answers
108 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 ...
Siddharth's user avatar
  • 823
-1 votes
1 answer
79 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 ...
Vetrivel's user avatar
7 votes
1 answer
193 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....
idka's user avatar
  • 81
3 votes
1 answer
70 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 ...
vigenary's user avatar
1 vote
1 answer
206 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 ...
XQY's user avatar
  • 111
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 ...
Siddharth's user avatar
  • 823
0 votes
1 answer
125 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....
NathanLiitt's user avatar
-1 votes
1 answer
78 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 = ...
llilibbou's user avatar
1 vote
0 answers
68 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: ...
Hirrolot's user avatar
5 votes
2 answers
331 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 ...
Bob's user avatar
  • 381
6 votes
0 answers
113 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 ...
vigenary's user avatar
8 votes
0 answers
113 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$.&...
Siddharth's user avatar
  • 823
6 votes
1 answer
361 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 ...
Hirrolot's user avatar
1 vote
0 answers
92 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)$, $\...
NathanLiitt's user avatar
1 vote
1 answer
96 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 ...
ghostOfTomJoad's user avatar
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 ...
Opt's user avatar
  • 1,311
0 votes
0 answers
65 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 ...
DenLilleMand's user avatar
4 votes
1 answer
140 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 ...
jpt4's user avatar
  • 81
2 votes
0 answers
98 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 ...
jpt4's user avatar
  • 81
3 votes
1 answer
393 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, ...
CrabMan's user avatar
  • 133
0 votes
0 answers
111 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 ...
Tomi Pannila's user avatar
2 votes
1 answer
175 views

Intuitive way to handle variable binding

Suppose we have an algebraic datatype parameterised by a type variable name, e.g. ...
A confused dove's user avatar
8 votes
3 answers
751 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 ...
paulotorrens's user avatar
7 votes
0 answers
136 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
4 votes
1 answer
190 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 ...
Nathan BeDell's user avatar
4 votes
0 answers
56 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-...
Ryan Kavanagh's user avatar
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 ...
Arjo's user avatar
  • 169
0 votes
0 answers
168 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 ...
user513093's user avatar
3 votes
0 answers
169 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
  • 823
2 votes
0 answers
74 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 ...
mudri's user avatar
  • 121
10 votes
0 answers
215 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 ...
gasche's user avatar
  • 2,040
-2 votes
1 answer
114 views

Resource for Understanding this Notation [closed]

I am trying to read this paper: https://arxiv.org/abs/1510.00925. I am familiar with grammars, but I cannot understand the notations in figure 1. Can anyone suggest a resource or book where I can ...
Mason's user avatar
  • 99
6 votes
1 answer
261 views

What are the pros and cons for type cases in dependent type theories?

Pattern matching on $\cal U$ is allowed in XTT and Idris2 (for unerased types), and that implies the injectivity of type constructors (that's just my intuition, though -- I also wonder how do I prove ...
ice1000's user avatar
  • 965
0 votes
1 answer
152 views

What does x.y notation mean?

In Harper's PFPL (Ed. 2, top of page 8), this notation is used but I don't see a definition. What does $x.y$ mean?
andi's user avatar
  • 71
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 ...
Martin Berger's user avatar
2 votes
0 answers
299 views

Are CCS and CSP still worth studying?

In Winskel's The formal semantics of programming languages 1993, Ch14 Nondeterminism and parallelism says This chapter is an introduction to nondeterministic and parallel (or concurrent) ...
Tim's user avatar
  • 639
0 votes
0 answers
548 views

What is the difference between a model of computation and a programming language?

https://en.wikipedia.org/wiki/Model_of_computation includes sequential models, functional models and concurrency models. Sequential models include finite state machine, Turing machines, random access ...
Tim's user avatar
  • 639
4 votes
1 answer
303 views

Is this variant of bitwise cyclic tag Turing-complete?

Cross-posted to MathOverflow. CT is an extremely minimalist programming language that can simulate arbitrary tag systems, and is therefore Turing-complete. A program consists simply of a string of 3 ...
user76284's user avatar
  • 662
2 votes
0 answers
78 views

Is there a list of notations developed for regular expressions? [closed]

There is, of course, PCRE. I know also of Olin Shiver's Structural Regular Expressions, and Rob Pike's Structural Regular Expressions. I also understand that Raku's regexps are different from perl's ...
honestSalami's user avatar
6 votes
2 answers
327 views

Intuition behind nested positivity and counterexamples

I'm looking at the nested positivity conditions for inductive types stated in the Coq manual. First off, are there any other references (not necessarily for Coq, but in dependent type theories ...
ionchy's user avatar
  • 325
1 vote
2 answers
205 views

Can concurrency models be compared in terms of some metrics?

In Seven Concurrency Models in Seven Weeks by Butcher, it compares Actor Model and Communicating Sequential Processes (CSP): CSP is more flexible than actor model: In actor model, the medium of ...
Tim's user avatar
  • 639
2 votes
1 answer
174 views

What graphs on $\mathbb{N}$ can be encoded as regular languages?

Suppose I represent the natural number 0 by "x", and use the symbol "s" for successor so that I get the following encoding of $\alpha : \mathbb{N} \rightarrow V$ of natural numbers ...
wanderingmathematician's user avatar
2 votes
1 answer
85 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: ...
Joey Eremondi's user avatar
2 votes
1 answer
145 views

Phonology and lambda calculus

I wonder whether there is any relationship between lambda calculus and phonology (study of phonemes). Specifically, how one would use the concepts of lambda calculus (typed or untyped) in the study of ...
Jacob Hjortmann's user avatar
1 vote
0 answers
119 views

λProlog vs HiLog

λProlog is a well-known higher-order logic programming language. On the other hand, HiLog is described as a logic programming language with higher-order syntax, but first-order model theory. Do I ...
MWB's user avatar
  • 231
3 votes
1 answer
98 views

Reference request: pi-calculus with simultaneous events

I am interested in using the $\pi$-calculus as a basis for modeling workflows, and came up with an extension that proved useful in my modeling, namely the ability to specify that two or more channel ...
Ulrik Rasmussen's user avatar
1 vote
1 answer
211 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
8 votes
2 answers
335 views

Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?

It is well known that any CCC (cartesian closed category) is a model of the simply-typed $\lambda$-calculus. It is less well known that System F admits a categorical model, but it is also well studied ...
xrq's user avatar
  • 1,175

1
2 3 4 5
8