Questions tagged [programming-languages]

Questions related to design, implementation, and analysis of programming languages. NOT for questions about how to program, which are off-topic on this site.

Filter by
Sorted by
Tagged with
1
vote
0answers
59 views

Mathematical resource material accompanying TAPL

I'm currently reading Types and Programming Languages by Benjamin C. Pierce and just arrived at chapter 21 Metatheory of Recursive Types. Prior to this chapter I found the book challenging but ...
2
votes
1answer
74 views

How do I count the exact number of executed commands for a MIPS program?

I want to know what the best way is to count the number of executed commands for a given MIPS program. Let's say we're given a simple for loop that counts from $0$ to $100$. For this I would write the ...
0
votes
2answers
2k views

Programming Language Hierarchy

I know that Assembly is the lowest level of the stack besides machine code, but are the languages above it all considered "high level languages" or is there a hierarchy amongst these languages. For ...
2
votes
3answers
114 views

Are there any programming languages which support user defined control structures?

For instance, the user would define a for each loop in their code as having a structure something like: foreach([variable1] : [variable2]){ [statements] } (...
2
votes
1answer
87 views

How to make an unambigous grammar of a programming language

We know that the decision problem of whether an arbitrary context-free grammar is ambiguous is undecidable. My question is how are made the unambigous grammar of programming language? My guessing is ...
1
vote
0answers
42 views

Sequential valid programs to find novel outputs?

I have: A programming language (P). Programs should take no input and produce a sequence of integers as output. A way to enumerate all valid programs in this language (R) in a way that each program ...
0
votes
1answer
80 views

How to draw a parsing tree according to syntax diagram?

I would really appreciate if someone can explain the syntax diagram itself and can help to build the parsing tree.
0
votes
1answer
27 views

Examples of interesting semantics to study during a small project for a graduate Semantics course

I have been following the course Concrete Semantics with Isabelle/HOL. At some point we are given the task to verify a program/extend some semantic construction/prove some mathematical fact. I ...
3
votes
1answer
71 views

Is there a generally accepted name for creating types that select a subset of other types?

Tl;Dr; Given: type A = { int: foo, int: bar } type B = select foo from A What is the name of the typing relationship between A and B? What is the name of the ...
1
vote
0answers
37 views

directed edges in an undirected graph [duplicate]

Undirected graph is given which has M edges and N vertices we have to convert every edge from u−v to u→v or v→u such that the total outdegree of every vertex is even. For example, consider a graph ...
2
votes
0answers
36 views

What are the pros and cons of context-oriented programming (COP)?

I have started reading about COP, but can't really get a grip of it. What I understand is that you use layers to let the software dynmically adapt depending on the context, and this would result in ...
3
votes
0answers
37 views

How do you resolve this paradox with the invariance theorem?

The invariance theorem of kolmogorov complexity states that for two different languages with complexity functions $K_1$ and $K_2$, we have $$\exists c.\forall s. K_1(s) \le K_2(s) + c$$ Here is an ...
1
vote
1answer
45 views

What are $(S,\Sigma)$-CCCs?

I was reading this and I was trying to understand the definition of $(S,\Sigma)$-CCC. The first requirement says: a mapping [[_]] : S → |C|, associating some object [[s]] ∈ |C| to any s ∈ S; ...
6
votes
2answers
320 views

LET REC recursive expression static typing rule

I'm taking a programming languages course and had a question regarding the typing rules for a recursive let rec expression in a static typing system. To be more ...
4
votes
3answers
1k views

Soundness and completeness w.r.t. programming languages

I'm studying programming languages (more specifically type systems) and came across a concept I couldn't quite wrap my head around: soundness and completeness. I'm taking a class, and according to my ...
0
votes
1answer
88 views

Composition of compostion as a functor

"Composition of Composition" (i.e., (.) . (.)) in Haskell), has type ...
1
vote
1answer
51 views

PL: What solves the type isomorphism $X \cong (X \rightarrow \mathbf{2})$?

In Practical Foundations for Programming Languages, on page 138 (page 156 of the pdf), it says: Requiring solutions to all type equations may seem suspicious, because we know by Cantor’s Theorem ...
0
votes
0answers
81 views

Why is Combinatorial Sketching for Finite programs possible?

I was reading Combinatorial Sketching for Finite Programs and wanted to understand why synthesis of the sketching language was possible/feasible. As far as I understand a partial program is ...
0
votes
1answer
535 views

First-order vs Higher-order Programs

Can someone explain the difference between first-order programs and higher-order programs in the context of programming languages? My understanding so far is that Functional Languages (most) use ...
0
votes
1answer
1k views

What is the difference between “algorithm,” “process” and “program”?

I am currently studying algorithms and algorithmic design, and I am confused those terms. What is the difference between them? Thank you.
0
votes
1answer
54 views

Would hypercomputation machines be capable of simulating/computing/programming everything?

If uncomputable numbers existed, could this hypercomputation machines compute them? Could hypercomputation compute all types of uncomputable things? Even truly inconsistent things? Even things that ...
7
votes
1answer
373 views

What is the difference between A-normalization and K-normalization in compilers?

Administrative normal form is a program intermediate representation in which each immediate instruction has a name. It is used in GHC and OCaml. K-normalized form is an intermediate representation in ...
1
vote
1answer
59 views

Meta Programming Operators

I have a basic understanding how operators work (bitwise, logical, unary, ternary, etc.), but I am confused how you define what the operator does so the machine knows how to treat the operator when ...
4
votes
1answer
112 views

What's the difference between environment and memory in terms of programming languages?

I've been reading up on programming languages to better my understanding with the textbook Essentials of Programming Languages (3e) - Friedman & Wand. In a chapter regarding the states of ...
1
vote
0answers
46 views

Is there a distinction between pointers and references? [closed]

If so, what are the similarities and differences between the two? I’ve only worked with properties while programming.
1
vote
0answers
65 views

Why the name static and dynamic in static and dynamic scoping

I am wondering, from where static and dynamic scoping got their names. After understanding the concept of static and dynamic scoping in C, what I assume is that whenever we failed to find out the ...
0
votes
1answer
28 views

CLRS pseudocode involving both subscripting and property access of a data structure

In Introduction to Algorithms, the stack data structure's enqueue operation has the following pseudocode ...
3
votes
0answers
64 views

An instance when you can eliminate propositional double negation in coq

Suppose st: string -> nat and X stands for the string 'X'. Given the hypothesis ...
2
votes
0answers
43 views

Why interaction net languages use interaction rules to represent their syntaxes?

What I have looked up into: here, here and here What I have learnt: What is an interaction net, its deduction & interaction rules, How deduction rules can be changed into interaction rules -- ...
0
votes
1answer
21 views

Is it possible to define a pairwise function that can either append to a tuple or make a tuple, potentially with nested tuples?

I lack the vocabulary to appropriately express the question succinctly, so I apologize if the title question is confusing. Suppose you can define a binary infix operator that produces tuples, and you ...
2
votes
2answers
91 views

How does one show $(\lambda x . (\lambda y.x))yx \equiv_{\beta} y$ in lambda calculus?

I wanted to show: $$ (\lambda x . (\lambda y.x))yx \equiv_{\beta} y $$ the definition of beta equivalence is on page 17 of these notes. I did a few attempts but got different things like $x$. I ...
2
votes
1answer
117 views

How do we show $\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x . x)$ in lambda calculus?

How do we show $$\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x . x)$$? I was going through the slides here and it asked to do the above but by page 16 of the slides we have not ...
1
vote
1answer
34 views

Showing that an equivalence relation on programs need not be a congruence

An optional exercise from Programming Language Foundations asks Can you think of a relation on commands that is an equivalence but not a congruence? An equivalence here refers to an ordinary ...
0
votes
1answer
82 views

Bounded Quantification: Full F<: intuition

I'm currently looking into Chapter 26 of Types and Programming Languages and am a bit confused by the "intuition" for Full F<: (p. 395): A type T = ∀X<:T1.T2 describes a collection of ...
3
votes
2answers
838 views

Do “compiler” and “assembler” correspond to frontend and backend phases of a compiler?

In Compilers: Principles, Techniques, and Tools (2nd Edition) 2nd Edition by Alfred V. Aho (Author), Monica S. Lam (Author), Ravi Sethi (Author), Jeffrey D. Ullman (Author) , Figure 1.5 gives a ...
2
votes
0answers
53 views

Are there any interesting terms in pure LF or $\lambda\Pi$?

In my searching, I've seen that if Church numerals are encoded in a dependently typed Lambda calculus, that we can't derive induction or that $0 \neq 1$. I know that LF and the dependently typed ...
3
votes
2answers
100 views

Are Bad churches inhabited?

In type theory, some inductively defined data types allow you to prove absurdity. For example ...
2
votes
4answers
160 views

How does one formally show that two lambda functions are $\alpha$ equivalent?

I was going through the following slides and I wanted to show the following: $$ \lambda x. x \equiv_{\alpha} \lambda y . y$$ formally. They define a an $\alpha$-conversion on page 15 as follows: $$ ...
-1
votes
1answer
43 views

Is it safe to assume that there would be no high level languages without existence of compilers/interpreters?

I am relatively new to computer science. There,s been something that i have been thinking now that i am studying how to make actual compilers. We are past the days of programming with binary and ...
3
votes
2answers
103 views

Why does the denotational semantics for a while loop have a existence quantifier?

I was going through these notes and they have the following operator on partial functions: $$ \mathcal F^{k}(\bot)(\sigma) = \left\{ \begin{array}{ll} \alpha( [\![s]\!]\sigma ) & [\![b]\!]\...
1
vote
0answers
64 views

Can I call my library an interpreter?

I am working on tiny programming language (for our specific tasks). It's a script language. It looks like a library for C++ that can execute a code of this language. This library parses a source code ...
1
vote
2answers
116 views

How is it that programs can be identified with partial functions for programming language semantics?

I was reading about denotational semantics Broadly speaking, denotational semantics is concerned with finding mathematical objects called domains that represent what programs do. For example, ...
0
votes
1answer
126 views

Understanding SLDNF-forest

I am trying to understand this program and the respective forest. This is from the book Logic,Programming and Prolog by Ulf Nilsson. Question: In the main tree, why from ←off_gound(a) can you ...
3
votes
1answer
45 views

Common name for a group of commands which break the linear structure of the program

I'm looking for a name of a group of all commands which are break the linear structure of the program. In C PL, they are: ...
0
votes
1answer
45 views

Basic control statements for Turing equivalence? [duplicate]

Apologies ahead of time, I don't fully understand what I'm asking... But, is it possible to program using only 'while loops' and still be Turing equivalent? Or more generally, can I do everything ...
3
votes
0answers
99 views

PL: How can I prove the type of something using “Inversion for Typing”?

I'm currently going through this book about programming languages, and in section 4.2, Lemma 4.2 it says this: Lemma 4.2 (Inversion for Typing). Suppose that $\Gamma \vdash e : \tau$. If $e = \texttt{...
1
vote
1answer
95 views

What other than programming does a computer science degree usually involve? [closed]

Programming courses are about 30% of my computer science degree. Also at my university, around 15-20% of the degree are applied math courses. What other areas/fields are covered? For the majority of ...
1
vote
1answer
1k views

Difference between Row Major Order and Column Major order

Let take a multi-dimensional array: $a[2][3][4]$ Here $a$ is a three-dimensional array, which means that it is a collection of two-dimensional array's. Therefore ...
5
votes
0answers
76 views

Which languages, if any, implemented parametric polymorphism before ML?

In particular, was there any kind of implementation at the time Christopher Strachey wrote Fundamental Concepts in Programming Languages? In that work, Strachey lists Ad Hoc and Parametric ...
0
votes
2answers
105 views

What are constraints on some new logic programming language and system?

As I understand, everyone can create logic programming language and system by declaring that the valid program of some logic programming language is the set of statements in the form: ...

1
3 4
5
6 7
17