PL Key Concepts

Deepak Definitions

These are some of the definitions that have shown up on comprehensive exams and 550 exams. (DA) signifies Deepak Approved, i.e. it got a check-mark. NI (not-incorrect) signifies that the answer was not marked off on an exam, but there was no visible check-mark.

• assertion: properties of the effect of executing a construct.
• atom: a relation applied to terms
• chain: a chain is a subset which is totally ordered
• clause: a disjunction of a finite set of literals S.2011 (DA)
• complete partially ordered set: a partially ordered set such that each of its chains has a unique least upper bound. S.2011
• continuous function as in denotational semantics:given a Chain $C$, a function $F$ is continuous iff $\forall$ $c \; \in \; C$, $F(\cup C)\;=\;\cup_{c \in C}F(c)$
  • The continuity condition says that you get the same result whether you first apply F to each member of the chain and then take their union, or take their union first and then apply F to the result. S.2011
• fixed point of a function: Given $ f :: D \rightarrow D$, $x \; \in \; D$ is a fixed point iff $f(x)\;=\;x$ S.2011
• greatest lower bound of a set with respect to a partial ordering: GLB$(x,y) \; = \; z\; | \; z \; \lt \; x,\; z \; \lt \; y, \; \Rightarrow \; \forall \; z' \; \lt \; x,\; z' \; \lt \; y,\; z' \; \lt \; z$ S.2011
• Herbrand Base : All predicate symbols applied on all ground terms in every possible way. S.2011
• Herbrand Interpretation: any subset of the Herbrand Base.
• Herbrand Model: A Herbrand Interpretation in which each clause is valid, where validity is defined as: a clause is valid iff for every ground substitution $\sigma(B_1),\; \sigma(B_2),\;...,\; \sigma (B_n)$ in the clause body, the ground substitution, $\sigma(H_i)$ is in the model as well. (DA)
  • A subset of the Herbrand Base such that the clause holds.S.2011
• Herbrand Universe: the set of all possible ground terms for a language. S.2011 (DA)
• Hoare triple: precondition, statement, and postcondition. S.2011
• Horn clause: a finite disjunction of literals in which at most one literal is positive.
  • A clause with at most one positive literal of the form <math> H \leftarrow B_1, B_2,...B_k,\; k\; \geq\; 0 </math> S.2011
• inductive loop invariant: a loop invariant that is preserved by the body of the loop. S.2011
• invariant: a set of conditions, which if true upon entering a loop are still true upon the loop exit. (DA)
• lattice: a partially ordered set in which any two elements have a unique suprenum (join) and an infinum (meet). S.2011
• least fixed point of a function: a fixed point which is less than or equal to all other fixed points according to some partial order. S.2011
• least upper bound of a set with respect to a partial ordering: Given a poset $P,\;x\;\in \;P,\; y \; \in \;P$, then $z$ is the least upper bound of $x,\;y$ iff $z\; \geq \;x, \; z\; \geq \; y$ and $\forall \; z'\; \geq \;x, \; z'\; \geq$, \; $z' \; \geq \; z$ S.2011
• literal: an atom or its negation.
• logic program: the conjunction of a finite set of Horn Clauses.
• loop invariant: a formula which holds true for every execution within a loop S.2011
• lower bound of a set with respect to a partial ordering: given a set $A$ and a subset $B$, $x \; \in \; A$ is an lower bound iff for all $y \; \in \; B, \; x \; \leq \; y$ S.2011
• minimal fixed point of a function: a fixed point which is strictly less than all other fixed points according to some partial order. S.2011
• minimal Herbrand Model: the intersection of all Herbrand Models (the meaning of a program). (DA)
• monotonic function (denotational semantics): $f\; ::\; PartialOrd_1 \; \rightarrow \; PartialOrd_2 \; x \; \geq \; y \; \Rightarrow \; f(x) \; \geq \; f(y)$
• most general unifier: a set of substitutions of the variable in the system of equations which includes all other valid variable assignments
• partial correctness: assuming termination then the output specification will be satisfied.
• partially ordered set: a set which is ordered by a reflexive, anti-symmetric, and transitive relation.
• precondition: a formula whose axioms hold before execution of a statement in a Hoare Triple. S.2011
• postcondition: a formula whose axioms hold after evaluating a statement of a Hoare Triple, and a given precondition. S.2011
• ranking function: a function mapping program states to sets with a well founded order.
• strongest post condition: given a Hoare Triple , $\{P\}\; S\; \{Q\}$, $Q$ is the strongest post condition if $\forall \; Q' \; \in \{P\}\; S\; \{Q'\},\; Q \; \Rightarrow \; Q'$ S.2011 (DA)
• Tarski’s fixed point theorem: let $(L,\;\leq)$ be a complete lattice. For some monotone increasing function $f\;:\;L\; \rightarrow\; L$, the set of all fixed points with respect to $f$ is a complete lattice with respect to $\leq$. S.2011
• total correctness: proof of termination and a satisfied output specification.
• unifier: set of substitutions which make two sides of equations equivalent. (DA)
• upper bound of a set with respect to a partial ordering: given a set $A$ and a subset $B$, $x \; \in \; A$ is an upper bound iff for all $y \; \in \; B, \; x \; \geq \; y$ S.2011
• verification condition: a condition to be proven in order to establish partial correctness of a program.
  • a pre or post condition with the appropriate axiom of substitution applied for a given statement. S.2011
• weakest precondition:given a Hoare Triple , $\{P\}\; S\; \{Q\}$, $P$ is the weakest pre condition if $\forall \; P' \; \in \{P'\}\; S\; \{Q\},\; P' \; \Rightarrow \; P$ S.2011
• well-founded ordering: For a set $B$ and an ordering $R$, $R$ is well founded if it does not allow an infinite chain of applications to $b_1,b_2,...b_n \; \in \; B$. (NI)
  • a relation that does not admit an infinite descending chain.
• well-founded relation a relation $R$, is well founded if for every non-empty subclass a $R$-minimal element exists. S.2011
• well-founded set: a set such that every non-empty subset has a minimum value.
• widening: over approximation of the least upper bound used to ensure termination of fixed point computation in a lattice of infinite height.

Haskell

Breadth First Numbering

George's BFS

data Tree a = E
            | T a (Tree a) (Tree a)
              deriving Show

bfnum :: Tree a -> Tree Int
bfnum t = head $ q 1 [t]
    where q i ts = dq i ts (q (i + length [a | T a _ _ <- ts])
                             (concat [[l, r] | T a l r <- ts]))
          dq i (T _ _ _:hs) (l:r:lrs) = T i l r:dq (i+1) hs lrs
          dq i (E:hs) (lrs) = E:dq i hs lrs

In another variant of this problem Darko has given used a different style of tree which has children in a list form with designated Empty Leaves. The following code works in that case and is very easy to understand. This was adapted from a great source at http://resources.aims.ac.za/archive/2008/christine.pdf

data Tree a = E
        | T a [Tree a]
        deriving Show

bfnum :: Tree a -> Tree Int
bfnum (T a xs) = T 1 (bfnum' 2 xs)

bfnum' :: Int -> [Tree a] -> [Tree Int]
bfnum' _ [] = []
bfnum' i (E:ts) = (E:(bfnum' i ts))
bfnum' i ((T a xs):ts) = ((T i chdn):prnts) where
        chdn = drop (length ts) (bfnum' (i+1) (ts++xs))
        prnts = take (length ts) (bfnum' (i+1) (ts++xs))

Sample Input:

let t = T 5 (T 4 (T 2 (E) (E)) E) (T 3 (T 1 E E) E)
let t = T 5 [(T 4 [(T 2 [E,E]), E]),(T 3 [(T 1 [E,E]), E])]

Compilers

Continuation Passing Style

• CPS
• Reaching
• Liveness