While reading the example given in [1]., I couldn't understand how the authors set up the logic to compute the weakest preconditions (wp) in their car example in section 4.2. The dynamics of the problem are given by - $x' = x + 0.1v$ $v' = v + 0.1a + \epsilon$ I don't see the authors working on the former equation, only the latter. In addition, while reading about wp from the book [2], I learned that one needs to come up with a suitable postcondition. I believe the postcondition here is $v <= 1$. Why did the authors start the wp computation using $v_1 <=1 \land v_2 <= 1$? Also, in the next step they do $v_1<=1 \land v_1 + 0.1a_1 + \epsilon_1 <= 1$. Why did they only expand the equation on the right of the conjunction? Here is how I imagined it should have been done (based on my very limited knowledge of wp computations - We have the equation $v' = v + 0.1a + \epsilon$ and we have a horizon of 2. Therefore, we write this equation 2 times (because that's how RL algorithms are unrolled) - $v_1 = v_0 + 0.1a_0 + \epsilon_0$ $v_2 = v_1 + 0.1a_1 + \epsilon_1$ Now we set up a postcondition on $v_2$ such that $v_2<=1$ and then work backwards. My understanding is probably wrong, but I'd like the reader to see where I am getting confused. Please let me know if any clarification from my side is needed. Regarding the relation between $x'$ and $x$ and also $v_2$ and $v_1$: My understanding here is that $x'$ represents the subsequent state of the variable $x$. This is because of the following line in the paper - "A policy, in interaction with the environment, generates trajectories (or rollouts) $x_0,u_0, x_1,u_1, \ldots, u_{n-1}, x_n$ where $x_0 \sim p_0$, each $u_i \sim \pi(x_i)$, and each $x_{i+1} \sim P(x_i, u_i)$." Here we can see that each state can be obtained from the subsequent state except the initial state. [1]. Anderson, Greg, Swarat Chaudhuri, and Isil Dillig. "Guiding Safe Exploration with Weakest Preconditions." International Conference on Learning Repre

I was reading a book titled "Essentials of Logic Programming.", most parts of the book are easy to understand. but now having a problem with Theme 45: incremental constructions of the minimal model. The relevant parts are shown below. Some notations: $P$ is a definite program, $B(P)$ is the Herbrand base of $P$, $G(P)$ is a ground instantiation of $P$, $MM(P)$ is a minimal model of $P$. Theme 45 explains the incremental constructions of the minimal model as follows. The method starts by choosing some interpretation $I_1 \subseteq B(P)$. Later on, we shall see that there is a preferred choice of $I_1$ and that not all choices are adequate. Choosing $I_1$ can be viewed as guessing which atoms have to be true in any model of $P$. Now consider any clause in $G(P)$ kind(Chris) q if body if our guess assigns true to all atoms in this body then an immediate consequence of that guess is that q should also be made true, for otherwise the clause as a whole would be made false. Our next iterate $I_2$ comprise just those heading atoms q made true by this argument. This new iterate will not necessarily contain all those body atoms which justified the introduction of the new atoms q; this does not matter - successive iterates will eventually introduce and retain all of these atoms which must be true in any model of the program. Consider this example of a program $P$ on the domain $H=\{ dov,chris\}$: kind(X) if nice (X) nice(X) whose ground instantiation $G(P$ is highly abbreviated form is kind(dov) if nice(dov) kind(Chris) if nice(Chris) nice(dov) (where K=kind, N=nice, D=dov,C=Chris) and suppose we choose $I_1= \{ kind(dov),nice(Chris)\}$. Applying the above method yields $I_2= \{ nice(dov), kind(Chris)\}$ and $I_3= \{ nice(dov), kind(dov)\}$ All further iterates merely replicates $I_3$, which is accordingly referred to as a fixpoint. We have, in fact, converged upon the minimal model $MM(P)$. Let me explain how I understand or did not understand this example. - is

For context, yesterday I posted Does the first incompleteness theorem imply that any Turing complete programming language must have undefined behavior?. Part of what prompted me to ask that question in the first place is that, awhile ago, someone on the learnprogramming subreddit told me something about the reason C++ in particular having so much undefined behavior is because, for it to not have undefined behavior, it would have to use a much more restrictive language model, but they didn't explain what that means exactly. I had also asked on Quora awhile ago about why C++ compilers don't always throw errors when a program contains undefined behavior and at least one answer mentioned something about it being fundamentally impossible to always detect undefined behavior at compile time and that this was related to the halting problem being undecidable. Those two things combined have me wondering about models of computing more generally -- my understanding is that all/most popular programming languages, including C++, are Turing complete, and since I was told the problem of detecting UB in C++ is fundamental and related to the halting problem, I thought that perhaps all Turing complete programming languages must have undefined behavior and C++ is just worse at hiding it than others. But judging from the answers to my above-linked question, I was mistaken about that. So my question now is, what conditions need to be imposed on a Turing complete language in order to guarantee that all possible programs written in the language will have fully defined behavior determined by the language specification? And, on a side note, does the answer have anything to do with the incompleteness theorems? I ask the latter question because the idea of defining a language for which all possible programs have fully defined behavior seems quite similar to the idea of defining an axiom system for which all possible theorems are provable/disprovable.

You know how programming languages can be based on Lambda Calculus or the Turing Machine and SQL is based on relational algebra. Is there any such thing for CSS or any foundation that could be used for styling languages in general if we were to design a new language from scratch? Styling and layout in general is something I'd expect to be possible to formalize mathematically, at least the layout and positioning part of it.

Why do we need the main function and can't we execute the code without it? Can't we just execute our code outside the main function by making our own function?

Given two types, T1 and T2, how does structural equivalence work when they're self-referential? Further, how do we go about proving it? ``` T1: struct { a: int, b: pointer to T2 } T2: struct { a: int, b: pointer to T1 } ``` I was attempting to create a directed graph, and by proving the directed graphs are equivalent, we can prove the types are equivalent. For example: $$G1: T1.b \rightarrow T2 \rightarrow T2.b \rightarrow T1 \rightarrow T1.b$$ $$G2: T2.b \rightarrow T1 \rightarrow T1.b \rightarrow T2 \rightarrow T2.b$$ I don't know if I'm the right track here or not.

In articles or Quora posts about category theory, I often find mentions of the programming language Haskell. I have little knowledge of category theory and even less of programming. Could someone please explain how category theory is important in Haskell?

I came across this recent Reddit thread, Thoughts on Botton vs Unit Types, but I don't understand what the similarities and differences are in regards to when you are creating a programming language. If you are creating a programming language, why do you need both a Bottom and a Unit type (as defined in the thread). For the sake of this discussion, let's call the bottom type a type that has no members. NIL in Common Lisp, Nothing in Scala, never in TypeScript, Never in Swift. This type can be used to indicate the return type of a function that never returns (a function that only throws an exception, for example). Let's call the unit type a type that has a single member. NULL and NIL in Common Lisp (the symbol NIL not to be confused with the type NIL), () and () in Haskel, Unit and () in Scala, Void and () in Swift. What exactly are the differences between the two as well? In my PL, I currently just have a `void` type, which is meant to mean "nothing" or "empty" or "null" I would think, but this throws into question what I am doing. It seems I need to add another type, but not sure how it fits in. Because then in Rust you have the `None` type, I don't see why I couldn't just make that the `void` type as well. That sort of stuff. What are the similarities and differences, and why do you need both?

Here is the last paragraph at page 441 of the paper ‘Covariance and Contravariance: Conflict without a Cause’ by Giuseppe Castagna: How is all this translated into object-oriented type systems? Consider a message $m$ applied (or “sent”) to $n$ objects $e_1$, …, $e_n$ where $e_i$ is an instance of class $C_i$. Suppose we want to consider the classes of only the first $k$ objects in the method selection process. This dispatching scheme can be expressed using the following notation: $$m(e_1, …, e_k | e_{k+1}, …, e_n).$$ If the type of $m$ is $\{S_i → T_i\}_i$, then the expression above means that we want to select the method whose input type is the $\text{min}_i \{S_i | (C_1 × … × C_k) ≤ S_i\}$ and then to pass it all the $n$ arguments. The type, say $S_j → T_j$, of the selected branch must have the following form: $$\underbrace{(A_1 × … × A_k)}_{S_j} → \underbrace{(A_{k+1} × … × A_n) → U}_{T_j}$$ where $C_i ≤ A_i$ for $1 ≤ i ≤ k$ and $A_i ≤ C_i$ for $k < i ≤ n$. If we want to override the selected branch by a more precise one, then, as explained above, the new method must covariantly override $A_1, …, A_k$ (to specialize the branch) and contravariantly override $A_{k+1}, …, A_n$ (to have type safety). I expected $C_i ≤ A_i$ for $1 ≤ i ≤ n$ (instead of $C_i ≤ A_i$ for $1 ≤ i ≤ k$ and $A_i ≤ C_i$ for $k < i ≤ n$), because the call $m(e_1, …, e_n)$ is not type safe if we allow some argument types to be greater than the parameter types of the selected method. Am I misinterpreting the paragraph or did the author make a mistake?

In his paper The Free Lunch Is Over: A Fundamental Turn Toward Concurrency in Software, Herb Sutter writes: The mainstream state of the art revolves around lock-based programming, which is subtle and hazardous. We desperately need a higher-level programming model for concurrency than languages offer today; I'll have more to say about that soon. Can somebody with more knowledge about his work answer what he is referring to? Did he say more about that later?