Skip to main content

Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

Filter by
Sorted by
Tagged with
3 votes
2 answers
296 views

Languages that lack contraction, weakening or exchange

When learning about generalized arrows, a question arised to me: Are there any languages (or potential languages) that lack one or more of the structural rules: contraction, weakeing and exchange? ...
Petr's user avatar
  • 2,601
2 votes
1 answer
148 views

Is there a sense in which we can say error returned from a function is the reverse of context?

This came up in a discussion about golang, but I think it applies more generally. Context in which a function is executed (specially in when we have RPCs) and error returned from a function seem to ...
Kaveh's user avatar
  • 21.6k
10 votes
2 answers
1k views

What kind of theoretical object corresponds to a C++ concept?

I am lacking a background in theoretical computer science but I would have liked to understand to what kind of theoretical objects C++ concepts corresponds to. Basically, C++ concepts allow to define ...
Vincent's user avatar
  • 307
2 votes
1 answer
120 views

Completeness of Constraint Typing (type inference) question regarding $\sigma'$

The theorem of completeness of type inference states the following: Suppose $\Gamma \vdash t:S| _{\mathcal{X}}C$, ...
lilott8's user avatar
  • 185
7 votes
0 answers
230 views

Relationship between Pataraia's theorem and inductive-recursive definitions?

Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
Neel Krishnaswami's user avatar
6 votes
1 answer
215 views

Graph rewriting with one-to-many pattern matching?

In the single-pushout approach to graph rewriting, many nodes in a pattern graph can be matched to a single node of a target graph. My question is if there is a notion of graph rewriting where the ...
James Koppel's user avatar
9 votes
2 answers
250 views

What's the definition of join on iso-recursive types?

In languages with subtyping, there is often a "join" operation defined to compute the least upper bound of two types. It's used in type-checking, for example to find the smallest type that covers both ...
Jonathan Schuster's user avatar
7 votes
2 answers
339 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 ...
Martin Berger's user avatar
3 votes
2 answers
193 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 ...
wlnirvana's user avatar
  • 173
7 votes
1 answer
370 views

Do we care about confluence because of unique normal forms?

Confluence implies uniqueness of normal forms, which is great. It is also much simpler to reason about, allowing more reusable proofs (indeed I don't imagine a way to prove UN directly for the $\...
Guido's user avatar
  • 181
2 votes
1 answer
370 views

Can recursion be replaced with a finite set of higher-order functions? [closed]

I am wondering if there is some proof that all recursive algorithms can be rewritten to use some known set of higher-order functions instead of recursion. I'm talking about functions like fold, map, ...
HillwoodMonkey's user avatar
6 votes
0 answers
183 views

Notions of Computability at Higher Type III

I've recently found a very nice survey paper called "Notions of Computability at Higher Type" by John R. Longley. The paper says it is part of a 3-part series, with the 3rd concerning non-extensional ...
Max New's user avatar
  • 1,685
15 votes
1 answer
3k views

Why do functional programming languages require garbage collection?

What's stopping ghc from translating Haskell into a concatenative programming language such as combinatory logic and then simply using stack allocation for everything? According to Wikipedia, the ...
Nicholas Grasevski's user avatar
10 votes
0 answers
433 views

Typed Lambda Calculus models and denotations

I'm trying to draw a general mental picture about the models and the denotational semantics of the typed lambda calculus, in its different variants. I'm particularly interested in how the semantics ...
chi's user avatar
  • 678
2 votes
0 answers
176 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 ...
Akram El-Korashy's user avatar
2 votes
1 answer
294 views

Damas-Milner-like subset of the calculus of constructions with global type inference

Damas-Milner is a subset of System Fω that gives up expressivity (type-level computation) for usability (type inference). The experience with Haskell and ML attests to the practical value of this ...
isekaijin's user avatar
  • 501
-2 votes
1 answer
108 views

Comparing 2 programs for equivalence w.r.t input - output pairs [closed]

I'm new to theoretical research. I have the following question: Given 2 different computer programs, each generating certain outputs for a given set of inputs. Assuming we are given the range of ...
musigma's user avatar
12 votes
2 answers
615 views

Implementing "Internal" Languages

One of the most practical consequences of the "Curry-Howard-Lambek" correspondence is that the syntax of many lambda-calucli/logics can be used to perform constructions in a sufficiently structured ...
Max New's user avatar
  • 1,685
1 vote
1 answer
153 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 ...
Adribar's user avatar
  • 31
3 votes
1 answer
186 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 ...
galois's user avatar
  • 131
9 votes
1 answer
360 views

A bicartesian closed category of strict complete partial orders (Hask)

It seems to be well-known that programming languages can't have sums, products and nontermination together. Q1. Is this true? Below (or in the above link I gave) is a partial argument. However, ...
Blaisorblade's user avatar
  • 2,059
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 ...
TomR's user avatar
  • 409
7 votes
1 answer
145 views

Confusions about the technique for verifying implementations of linearizable objects in [Herlihy and Wing, 1990]

In Section 4.3.2 entitled "Proof Method" of Herlihy and Wing, "Linearizability: A Correctness Condition for Concurrent Objects", 1990 the authors describe the technique for verifying ...
hengxin's user avatar
  • 2,329
18 votes
2 answers
2k views

Status quo of category theory and monads in theoretical computer science research?

Background. I am a bachelor student who is interested in research related to category theory, monads and Haskell, and I want to find a topic for my bachelor’s thesis in that area. I have looked at ...
k.stm's user avatar
  • 281
15 votes
1 answer
590 views

Logical Reations for an Impredicative System in a Predicative MetaTheory

Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in ...
Max New's user avatar
  • 1,685
2 votes
1 answer
466 views

Is my language Turing-complete?

Consider a language like Brainfuck but without the brackets. At the end of each line (i.e. when "\n" occurs), if the current cell is not 0, then the line is re-executed. An example of an infinite ...
Filippo Costa's user avatar
6 votes
0 answers
461 views

How can unification be applied to interaction combinators?

The problem of unifying interaction combinators is probably undecidable since those are turing complete. As opposed to the lambda calculus, there is nothing like a simple type theory for interaction ...
MaiaVictor's user avatar
  • 3,147
5 votes
1 answer
306 views

How can you encode natural numbers operations on interaction combinators?

The church-encoding for natural numbers is a natural mean of implementing addition, multiplication and so on on the lambda calculus. Interaction nets are said to be an alternative universal ...
MaiaVictor's user avatar
  • 3,147
10 votes
2 answers
745 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 ...
Clément's user avatar
  • 281
16 votes
4 answers
777 views

Program reasoning about own source code

The inspiration for this question is the following (vague) question: What are the programming language/logical foundations for having an AI which could reason about its own source code and modify it? ...
Holden Lee's user avatar
12 votes
1 answer
459 views

An example where smallest normal lambda term is not fastest

Let the $size$ of $\lambda$-terms be defined as follows: $size(x) = 1$, $size(λx.t) = size(t) + 1$, $size(t s) = size(t) + size(s) + 1$. Let the complexity of a $\lambda$-term $t$ be defined as the ...
MaiaVictor's user avatar
  • 3,147
4 votes
1 answer
75 views

Is infinitary Böhm-reduction wrt. root-active terms for $\lambda$-calculus transitive?

I expect the answer to be "obviously yes", but to my inexperienced eye, that's not directly obvious, because the definition of infinite Böhm-reduction does not include a transitivity rule (it wouldn't ...
Blaisorblade's user avatar
  • 2,059
3 votes
1 answer
165 views

Is there a pair of different lambda terms in the normal form that behave identically when applied to any input?

Let f and g be lambda terms in the normal form, such that f is intensionally different from <...
MaiaVictor's user avatar
  • 3,147
3 votes
1 answer
350 views

Actual practical example of a prefix-free Turing-complete language

A theoretical construct that comes up a lot in algorithmic computability theory is a universal prefix-free language. For my purposes, this is a language with the following properties: its syntax is ...
N. Virgo's user avatar
  • 699
13 votes
3 answers
901 views

For what languages is there already a theory of observational equivalence?

For a correctness proof, I'm looking for a usable notion of program equivalence $\cong$ for Barendregt's pure type systems (PTSs); missing that, for enough specific type systems. My goal is simply to ...
Blaisorblade's user avatar
  • 2,059
4 votes
3 answers
507 views

Distinguishing semantics vs syntactic techniques and the syntax of your semantic domains

Consider a denotational semantics from simply-typed $\lambda$-calculus into dependent type theory. Is that actually a (trivial) term transformation into that dependent type theory? After all, type ...
Blaisorblade's user avatar
  • 2,059
7 votes
1 answer
387 views

Can type inference be classified in two groups: unification-based and control-flow-based?

I recently came across the 1995 paper Safety analysis versus type inference (pdf link) by Palsberg and Schartzbach that contrasts unification-based type inference and static analysis methods based on ...
hugomg's user avatar
  • 173
6 votes
1 answer
139 views

In which posets is the set of compact elements downwards closed?

In a poset $(D, \sqsubseteq)$, a compact element is an element $d \in D$ such that for every directed set $A$ which happens to have a supremum $\bigsqcup A \in D$ with $d \sqsubseteq \bigsqcup A$, it ...
Basil's user avatar
  • 361
12 votes
1 answer
318 views

Reference for the fact that (0=1) implies false requires a universe in MLTT

It's a fairly well-known fact that deriving a contradiction from a disequality (for example, $(0=1) \to \bot$) in Martin-Loef type theory requires a universe. The proof is also fairly ...
Neel Krishnaswami's user avatar
2 votes
2 answers
251 views

What is the formalism behind ?- (query) in Prolog?

I am in general interested in a more formal (better be logical, as in related to mathematical logic) definition of a query. As an example, there's Prolog operator ...
wvxvw's user avatar
  • 167
0 votes
0 answers
173 views

Is there an algorithm to find whether 2 combinators form a Turing-complete system?

It is known that K = (λx.(λy.x)) and S = (λx.(λy.(λz.((x z) (y z))))) define a turing complete system, and we know procedures to ...
MaiaVictor's user avatar
  • 3,147
0 votes
2 answers
467 views

Converting a Hardware description language to a functional programming language [closed]

I am looking for some guidelines on converting a Hardware description language such as VHDL or Verilog to a Typed Language. The reason I want to do this is to formally verify a hardware whose ...
jhenry's user avatar
  • 27
3 votes
1 answer
315 views

understanding programming monads through diagrams

I am trying to understand better how the category definition of monad is related to the computer science definition. nlab has a rather terse definition of Monad in terms of a bicategory. an object $...
john mangual's user avatar
19 votes
1 answer
915 views

Scott's stochastic lambda calculi

Recently, Dana Scott proposed stochastic lambda calculus, an attempt to introduce probabilistic elements into (untyped) lambda calculus based on a semantics called graph model. You can find his ...
Pteromys's user avatar
  • 895
25 votes
5 answers
2k views

Are there any annotated formal verification systems for pure functional programming languages?

ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified. I have not looked into it, but I imagine that the ...
Nathan BeDell's user avatar
3 votes
0 answers
112 views

How to analyze the quality of data definition language? [closed]

I know that DDL is most often used when talking about databases, but I see no reason why XML, PDF or even to some extent Prolog shouldn't belong to this category. It looks like branches of CS ...
wvxvw's user avatar
  • 167
7 votes
2 answers
216 views

Call-by-push-value's denotational semantics of "thunk diverge"

I was reading about Call-by-Push-Value in the introducing paper from 1999, but I have some confusion, partially because of my unfamiliarity with domain theory. I might have figured it out, but I'd ...
Blaisorblade's user avatar
  • 2,059
35 votes
5 answers
13k views

What are some good introductory books on type theory?

I'm recently studying Haskell and programming languages. Could someone recommend some books on type theory?
qazwsx's user avatar
  • 559
6 votes
1 answer
459 views

Describing state machines mathematically

The short paper "Computer Science and State Machines" by Leslie Lamport seems quite strange to me. On the one hand, I am surprised to see that an important hardware protocol called "two-phase ...
hengxin's user avatar
  • 2,329
6 votes
1 answer
376 views

Type theory for memory safe data structures

Data structures such as a doubly linked list and a B+ tree have blocks of memory that have multiple pointers to it. This creates the risk that a bug will allow memory to be accessed after being freed. ...
user782220's user avatar

1 2
3
4 5
8