This part is not shown on PFPL preview version.

Introduction

Many programs are instances of a pattern in a particular situation. Sometimes types determine the pattern by a technique called (typed) generic programming.

Example: the natural number definition in Chapter 9 defines pattern of recursion on values of an inductive type, which is expressed as a generic program.

Consider a function $f:\rho\to\rho’$, we wish to extend $f$ to a transformation from type $\lbrack \rho/t\rbrack\tau$ to $\lbrack \rho/t\rbrack\tau$ by applying $f$ to various spots in the inputs, where $\rho$ occurs to obtain a value of type $\rho’$, leaving the rest of data structure alone.

$\tau$ can be $\text{nat}\times t$ and $f$ can be extended to $\text{nat}\times\rho\to\text{nat}\times\rho’$ that transform $\langle a,b\rangle$ to $\langle a,f(b)\rangle$.

Ambiguity and Type Operator

Ambiguity arises in many-one nature of substitution. A type can have the form $\lbrack\rho/t\rbrack\tau$ in different ways, according to how $t$ occur in $\tau$.

The ambiguity is resolved by giving a template that marks the occurrences of $t$ in $\tau$ at which $f$ is applied.

Such template is known as type operator $t.\tau$, which is a abstractor binding type variable $t$ and type $\tau$.

The part is not shown on PFPL preview version.

From Constructive Logic to Classical Logic

Constructive logic is a logic of positive evidence, as stated in last chapter.

In contrast, classical logic is a logic of perfect information where every proposition is either true or false.

This casts a “god’s view” of the world, where there are no open problems, all propositions converge to a result. The symmetry between truth and falsity is appealing, but the logical connectives are weaker in classical case.

In Exercise 12.1 for LEM, LEM is not universally valid. It is valid only under classical case.

Constructive logic is stronger (more expressive) than classical logic since it can express more distinctions (between affirmation and irrefutability) and it is consistent with classical logic.

A proof in classical logic is a computation that cannot be refuted.

Computationally, a refutation consists of a continuation, or control stack, that takes a proof of proposition and derives a contradiction. A proof in classical logic is a computation that, when given a refutation of that proposition derives a contradiction, witnessing the impossibility of refuting it.

This part is not shown on PFPL preview version.

What is Constructive Logic

Constructive logic codifies the principles of mathematical reasoning as it is actually practiced.

In mathematics, a proposition is judged true exactly when it has a proof, and false exactly when refutation occurs. Since there’re always, and will always be, unsolved problems, we can’t expect in general a proposition be either true or false.

Please refer this link from page 87 to 94.

From Product to Sum

The binary sum type offers a choice of two types, and the nullary sum offers a choice of no things.

Finite sums generalize binary and nullary sums to allow an arbitrary number of cases indexed by a finite index set.

As with products, sums comes in with both eager and lazy variants, differs in how values of sum types are defined.

Please refer this link from page 81 to 85.

From Unit to Finite Product

Binary product of two types consists of ordered pairs of values, one from each type in order specified.

Nullary product or unit type consists solely of unique “null tuple” of no value.

Associated elimination form of binary product is projection, which select first/second of the pair. No associated elimination form exists for nullary product.

Product types admits both lazy and eager dynamics:

• In lazy dynamics, a pair is a value without regard to whether its components are values, they are not evaluated until (if ever) they are accessed and used in another computation.
• In eager dynamics, a pair is a value only if its components are values; they are evaluated when the pair is created.

Finite product with form $\langle \tau_i \rangle_{i\in I}$ is a more general form, indexed by a finite set of indices $I$.

The components are accessed by $I$-indexed projection operations, generalizing the binary case. Similar to binary product, finite products admit both an eager and a lazy interpretation.

Please refer this link from page 71 to 78.

From E to T

System T is the combination of function types with the type of natural numbers. T provides a general mechanism called primitive recursion.

Primitive recursion captures essential inductive character of natural numbers, hence may be seen as intrinsic termination proof for each program in that language.

Consequently we may only define total functions in that language, those that always return a value for each argument.

The proof may seem like a shield against infinite loops, it is a weapon that can be used to show that some programs cannot be written in T.

This part is not shown on PFPL preview version.

Functions as Language Extensions

A function is defined by binding a name to an abt with a bound variable serves as the argument.

A function is applied by substitute a particular expression of suitable type for a bound variable to get an expression.

First-order functions have domain and range limited to num and str.

Higher-order functions permit arguments and results to be other functions.

Please refer this link from page 55 to 60.

Another Forms of Dynamics

An evaluation dynamics is a relation between a phase and its value that is defined without detailing step-by-step evaluation process with notation $e \Downarrow v​$.

Cost dynamics enriched evaluation dynamics with cost measure specifying resource usage for evaluation as $e \Downarrow ^k v​$.

Please refer this link from page 49 to 54.

Intros

Type safety expresses the coherence between the statics and the dynamics. Statics may be seen as predicting that the value of an expression will have a certain form so that the dynamics of the expression will be well-defined. Thus, evaluation will not get stuck.

The theorem of type safety for E is defined as:

• (Preservation) If $e : \tau$ and $e \longmapsto e’$, then $e’: \tau$.
• (Progress) If $e : \tau$ and either $e \text{ val}$ or $\exists e’$ such that $e \longmapsto e’$.

Safety is the conjunction of preservation and progress.

$e \text{ stuck}$ iff $\neg e \text{ val}$ and $\not\exists e’$ such that $e \longmapsto e’$. Based on safety theorem, stuck state is necessarily ill-typed.

Please refer this link from page 41 to 48.

Dynamics Keywords

Dynamics of a language describes how programs are executed.

• Structural Dynamics: Defines transition system inductively specifies step-by-step process of executing a program.
• Contextual Dynamics: A variation of structural dynamics.
• Equational Dynamics: A collection of rules defining when one program is definitionally equivalent to another.

Please refer this link from page 35 to 40.

PL Phase Distinction

There are 2 phases defined in PLs:

• Static
  • Parsing and Type Checking to ensure the program is well-formed.
• Dynamic
  • Well-Behaved Execution of well-formed programs.

A language is said to be safe when well-formed and well-behaved execution are both achieved.

What about Static Phase

Static phase is specified by a statics comprising a set of rules for deriving type judgments stating that an expression is well-formed of a certain type.

Type safety tells us that the predictions about “some aspects of run-time safety by seeing that the types fit well in the program” is correct.

This note will use PFPL expression language E as example.

Please refer this link from page 23 to 32.

Keywords

• Hypothetical Judgments: an entailment between one or more hypotheses and a conclusion.
• Entailment has 2 notions:
  • derivability
  • admissibility
• General Judgment: the universality or genericity of a judgment.
• General Judgment has 2 forms:
  • generic
  • parametric

Please refer this link from page 13 to 21.

Framework of Inductive Definitions

This chapter is the development of basic framework of inductive definitions.

An inductive definition consists of a set of rules for deriving judgments.

Judgments are statements about one or more abt’s of some sort.

The rules specify necessary and sufficient conditions for the validity of a judgment, hence fully determine its meaning.

Please refer this link from page 3 to 11.

Here is the problem link.

This problem is all about BFS, but it really points out some of my weak points.

I almost cried in the library since this problem had bothered me for such a long time, I tried so hard, and I succeeded after all! Cheers!

Here is a very beautiful solution using dynamic programming with $O(n)$ time complexity.

Personally, I think dynamic programming is very important for a coder. This is not a specific skill but a kind of idea or method of thinking. This helps you get a global optimal result step by step from the easiest condition to the current condition, which is the task we need to solve.

Since I don’t have much experience in coding and I just do it for fun, I hope my code can bring you some happiness and understnading here…

This is just USACO 1.1, easy. But the problem afterwards are hard…

Actually, I unfortunately failed in round1. But I find algorithm hacker cup interesting. I wrote some codes as the solutions for this round. Hope you enjoy it.