Maths - Semantics

Judgment

"an object of knowledge"

A typing declaration is something of this form

where

• t is a term.
• T is the type.

due to Curry-Howard this could be either:

• t is a proof of T
• t is a program which has type T

ref

We have types and terms. A term may be either a value (a canonical term) or something that can be computed to a term.

Canonical form of function is a λ-expression.

'a' is type 'A' or 'a' computes to a value of type 'A'.
'a' is a proof of 'A'

Assumptions

Context

In a type system these are type assumptions for the (free) term variables.

Separated by commas. All assumed to be true

each one is like a parameter to a 'constructor'.

For instance 'a' can be assigned type A using the type assumptions

premises

conclusion

In the logic of conditionals this is called the antecedent

In the logic of conditionals this is called the consequent.

There are variations on this notation. The diagram on the right illustrates the notation in the 'Categories for Types', Roy L. Crole book.

In this notation the syntax (function signatures) is separated from the semantics.

Here is a version from the same book for equations.

Note here equations are not shown as types in a Curry-Howard way.

On the proof theory page about propositional logic (here) we have rules like the elimination rule for \/.

If A\/B then we can say that at least one of them is true. To codify this more formally we use assumptions:

Identity Rule

we can go from assumption to conclusion.

Cut Rule

This goes in the opposite direction.

This is a generalisation of 'modus ponens ' or 'implication elimination'. The cut-elimination theorem states that any judgement that possesses a proof making use of the cut rule also possesses a cut-free proof (we can inline the proof)

Sometimes the cut rule is a primitive built into the mechanism.

Weakening Rule

Hypotheses may be extended with additional members

Contraction Rule

Two equal (or unifiable) members on the same side of a sequent may be replaced by a single member.

Hypotheses contains two proofs of of A that is x:A y:A which we can replace with one proof z:A .

Also known as:

• factoring in automated theorem proving systems using resolution.
• 'idempotency of entailment' in classical logic.

Exchange Rule

variables in the context can be reordered. (for dependent types B cannot depend on a.)

This rule shows how a variable can be removed using substitution.

(relationship to removing a variable by function application : lambda elimination)

=1

Girard's linear logic does not allow the copying and destruction of terms so they must be used once. However they are still transferable. (transferring a resource from one owner to another can be done even when the resource cannot be copied.)

β-reduction - see below

introduction -> elimination = computed by substitution .

Constructor builds structure

May be multiple constructors, but only one of them is required to create a structure.

Destructor decompose structure

Often by pattern matching (case statement)

We are choosing between A and B, if we have a constructor followed by a distructor (Beta reduction) we can either make the choice at the constructor or the distructor stage.

where

• T is the type of the recursor
• U is the universal type

unit

(just ignore argument of unit type)

empty (bottom)

no constructor

boolean

formation rule

term eliminator rule

assume: a implies c
and b implies c

computation rule

beta reduction

match(inl(a), x.c_A y.c_B) =>_β c_A[a/x]
match(inr(b), x.c_A y.c_B) =>_β c_B[b/x]

Idris

we could define a sum type like this:


data Or : Type -> Type -> Type where
   OrIntroLeft : a -> A a b
   OrIntroRight : b -> A a b

also there is a built in type 'Either':

from : Idris-dev/libs/prelude/Prelude/Either.idr

||| A sum type
data Either : (a, b : Type) -> Type where
  ||| One possibility of the sum, 
  ||| conventionally used to represent errors
  Left : (l : a) -> Either a b
  ||| The other possibility, conventionally
  ||| used to represent success
  Right : (r : b) -> Either a b

-- Usage hints for erasure analysis
%used Left l
%used Right r

--------------------------------------------------------------------------------
-- Syntactic tests
--------------------------------------------------------------------------------

||| True if the argument is Left, False otherwise
isLeft : Either a b -> Bool
isLeft (Left l)  = True
isLeft (Right r) = False

||| True if the argument is Right, False otherwise
isRight : Either a b -> Bool
isRight (Left l)  = False
isRight (Right r) = True

--------------------------------------------------------------------------------
-- Misc.
--------------------------------------------------------------------------------

||| Simply-typed eliminator for Either
||| @ f the action to take on Left
||| @ g the action to take on Right
||| @ e the sum to analyze
either : (f : Lazy (a -> c)) ->
           (g : Lazy (b -> c)) ->
           (e : Either a b) -> c
either l r (Left x)  = (Force l) x
either l r (Right x) = (Force r) x

COQ

from : coq/theories/Init/Datatypes.v

(** [sum A B], written [A + B], is
     the disjoint sum of [A] and [B] *)

#[universes(template)]
Inductive sum (A B:Type) : Type :=
  | inl : A -> sum A B
  | inr : B -> sum A B.

Notation "x + y" := (sum x y) : type_scope.

Arguments inl {A B} _ , [A] B _.
Arguments inr {A B} _ , A [B] _.

formation rule

So the A×B type 'remembers' its formed from an A type and a B type?

term introduction rule

(a,b) is a tuple

term eliminator

Two projections fst (first) and snd (second) sometimes called p₁ and p₂

Local completeness rule

eta reduction rule

Ensures elimination rule not too weak (information not lost)

Idris

We can have a type which corresponds to conjunction:

data And : Type -> Type -> Type where
   AndIntro : a -> b -> A a b

There is a built in type called 'Pair'.

from : Idris-dev/libs/prelude/Builtins.idr

  ||| The non-dependent pair type, also known as conjunction.
  ||| @A the type of the left elements in the pair
  ||| @B the type of the right elements in the pair
  data Pair : (A : Type) -> (B : Type) -> Type where
     ||| A pair of elements
     ||| @a the left element of the pair
     ||| @b the right element of the pair
MkPair : {A, B : Type} -> (1 a : A) -> (1 b : B) -> Pair A B

||| Return the first element of a pair.
fst : (a, b) -> a
fst (x, y) = x

||| Return the second element of a pair.
snd : (a, b) -> b
snd (x, y) = y

COQ

from : coq/theories/Init/Datatypes.v

(** [prod A B], written [A * B], is the product of [A] and [B];
    the pair [pair A B a b] of [a] and [b]
    is abbreviated [(a,b)] *)

#[universes(template)]
Inductive prod (A B:Type) : Type :=
  pair : A -> B -> A * B

where "x * y" := (prod x y) : type_scope.

Add Printing Let prod.

Notation "( x , y , .. , z )" :=
            (pair .. (pair x y) .. z) : core_scope.

Arguments pair {A B} _ _.

Register prod as core.prod.type.
Register pair as core.prod.intro.
Register prod_rect as core.prod.rect.

Section projections.
  Context {A : Type} {B : Type}.

  Definition fst (p:A * B) := match p with (x, y) => x end.
  Definition snd (p:A * B) := match p with (x, y) => y end.

  Register fst as core.prod.proj1.
  Register snd as core.prod.proj2.
End projections.

formation rule

term introduction rule

assume a implies b

(given a proof of A we get a proof of B)

lambda abstraction:

Γ a:Ab:B		ΓB:Type
Γλa.b : A -> B

term eliminator

Modus Ponens

application:

ΓA->B:Type		Γa:A
Γf(a) : B

computation rule

substitution - in this case of a for x.

( λ x . b(x)) (a) =>_β b(a)

we reduce this by substitution.

b[a/x]

Local completeness rule

eta reduction rule

Idris

from : Idris-dev/libs/prelude/Prelude/Basics.idr

||| Function application.
apply : (a -> b) -> a -> b
apply f a = f a

formation rule

It exists

term introduction rule

Local completeness rule

Idris

from : Idris-dev/libs/prelude/Builtins.idr

||| The empty type, also known as the trivially false proposition.
|||
||| Use `void` or `absurd` to prove anything if
||| you have a variable of type `Void` in scope.
data Void : Type where

||| The eliminator for the `Void` type.
void : Void -> a
  

COQ

from : coq/theories/Init/Datatypes.v

(** [Empty_set] is a datatype with no inhabitant *)

Inductive Empty_set : Set :=.

Unit is always true, we can introduce a term without any additional information.

There is a sense that this is the inverse of the empty type:

• empty type can not be introduced
• unit type can always by introduced

formation rule

Unit type exists and does not depend on anything.

term introduction rule

Unit is always true, we can introduce a term without any additional information.

term eliminator

p:unit /\ c = c

If we know how to produce a C using all the possible inputs that can go into a unit, then we can produce a C from any unit.

computation rule

When we evaluate the eliminator on a term of canonical form, we obtain the data that went into the eliminator associated with that form

Local completeness rule

Idris

from : Idris-dev/libs/prelude/Builtins.idr

||| The canonical single-element type, also known as the trivially
||| true proposition.
data Unit =
  ||| The trivial constructor for `()`.
  MkUnit

COQ

from : coq/theories/Init/Datatypes.v

(** [unit] is a singleton datatype with sole inhabitant [tt] *)

Inductive unit : Set :=
tt : unit.

formation rule

Id exists for every pair of terms in A

term introduction rule

reflexitvity

Local completeness rule

Idris

from : Idris-dev/libs/prelude/Prelude/Basics.idr

||| Identity function.
id : a -> a
id x = x

COQ

from : coq/theories/Init/Datatypes.v

(** [identity A a] is the family of
    datatypes on [A] whose sole non-empty
    member is the singleton datatype [identity A a a] whose
    sole inhabitant is denoted [identity_refl A a] *)

#[universes(template)]
Inductive identity (A:Type) (a:A) : A -> Type :=
  identity_refl : identity a a.
Hint Resolve identity_refl: core.

Arguments identity_ind [A] a P f y i.
Arguments identity_rec [A] a P f y i.
Arguments identity_rect [A] a P f y i.

Register identity as core.identity.type.
Register identity_refl as core.identity.refl.
Register identity_ind as core.identity.ind.

(** Identity type *)

Definition ID := forall A:Type, A -> A.
Definition id : ID := fun A x => x.

Definition IDProp := forall A:Prop, A -> A.
Definition idProp : IDProp := fun A x => x.

formation rule

dont really need to have two copies of Unit, just making the point this is a sum.

term eliminator

assume: a implies c
and b implies c

beta reduction

match(inl(a), x.c_A y.c_B) ->_β c_A[a/x]

match(inr(b), x.c_A y.c_B) ->_β c_B[b/x]

Local completeness rule

formation rule

term introduction rule

Local completeness rule

formation rule

term introduction rule

Local completeness rule

formation rule

N exists

term introduction rules

term eliminator

Proof by induction

To prove property P (implemented as a type) we need to proove P(0) and P(x) implies P(sx)

rec is recursor (see recursor section above) where:

rec nat z₀ z_s O = z₀
rec nat z₀ z_s( S n) = z_s (n ,(rec nat z₀ z_s, n))

where

• z₀ is the value returned for zero.
• z_s is the value returned for succesor.

formation rule

term introduction rules

term eliminator

A bit like an introduction rule or like 'return' in monad.

• E is a proof/computation that might not terminate.
• in the context that 'x is a proof that A is true' then 'F is a proof that C is lax'

A bit like a substitution rule or like 'bind' in monad.