Questions tagged [pl.programming-languages]
Programming languages, in particular, focussing on their semantics.
372
questions
3
votes
0
answers
69
views
Can a positive elementary inductive definition refer to its own stage comparison relation?
Suppose $\varphi(x,S)$ is a positive elementary formula, i.e., a first-order formula with second-order relation variable $S$, such that the arity of $x$ and $S$ agree. In this setting, $\varphi$ can ...
- 803
-1
votes
1
answer
71
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 ...
- 99
7
votes
1
answer
187
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....
- 81
3
votes
1
answer
67
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 ...
- 93
1
vote
1
answer
200
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 ...
- 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 ...
- 803
0
votes
1
answer
115
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....
- 11
-1
votes
1
answer
67
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 = ...
1
vote
0
answers
64
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:
...
- 73
5
votes
2
answers
323
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 ...
- 381
6
votes
0
answers
111
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
8
votes
0
answers
110
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$.&...
- 803
6
votes
1
answer
303
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 ...
- 73
1
vote
0
answers
90
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
86
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 ...
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
0
votes
0
answers
64
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
135
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 ...
- 81
2
votes
0
answers
93
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 ...
- 81
3
votes
1
answer
375
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, ...
- 133
0
votes
0
answers
106
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
171
views
Intuitive way to handle variable binding
Suppose we have an algebraic datatype parameterised by a type variable name, e.g.
...
8
votes
3
answers
739
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 ...
- 377
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
4
votes
1
answer
184
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 ...
- 603
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-...
- 141
6
votes
3
answers
1k
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 ...
- 169
0
votes
0
answers
162
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 ...
- 119
3
votes
0
answers
167
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
2
votes
0
answers
73
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
10
votes
0
answers
211
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
-2
votes
1
answer
113
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 ...
- 99
6
votes
1
answer
248
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 ...
- 965
0
votes
1
answer
151
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?
- 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 ...
- 11.4k
2
votes
0
answers
296
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) ...
- 639
0
votes
0
answers
526
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 ...
- 639
4
votes
1
answer
291
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 ...
- 652
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 ...
- 121
6
votes
2
answers
321
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 ...
- 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 ...
- 639
2
votes
1
answer
171
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 ...
2
votes
1
answer
83
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:
...
- 2,830
2
votes
1
answer
142
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 ...
1
vote
0
answers
116
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 ...
- 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 ...
- 420
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
8
votes
2
answers
324
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 ...
- 1,175
3
votes
1
answer
237
views
Why would the term "dynamically typed" be considered a misnomer?
In the book "Types and Programming Languages", the author writes:
The word "static" is sometimes added explicitly - we speak of a "statically typed programming language",...
- 43
1
vote
0
answers
34
views
Non Turing-Complete Models, Conditional-Complete function?
I know well the distinction between the class of Partial Recursive Functions, and $\mu$-Recursive, i.e. the latter is Turing Complete and the former is equivalent to the LOOP-Program model of ...
