-
SCW Office hours: Wednesday morning, 9-11
-
Submit Ch9.v (only 1 person has so far). But don't stress; homework is intended to be diagnostic. If you are having trouble, come see me and we will work through it.
-
Don't forget to send questions (7/12 did today)
-
Make sure you are using the second edition, and you are reading Chapters not Parts.
=========================================================================
Questions about primitive recursion? Especially how it is implemented in Coq in systemt.ott?
Ott can only bind 1 variable per rule, so I pushed the "y" variable into the e1 term by requiring it to be a function value. (Requiring it to be a value is not actually necessary, but better matches the book.)
G |- e : nat
G |- e0 : t
G , x : nat |- e1 : t -> t
e1 val
----------------------------------------- :: rec
G |- rec e { z -> e0 ; s x -> e1 } : t
Plan
- Introduce products
- Goedel's System T review and primitive recursion
- Why products?
Start with language from before and add new type forms for unit and products:
t ::= nat | t1 -> t2 | unit | t1 * t2
For expressions,
e ::= ... | () -- unit, represents "nothing" the empty product
| (e1,e2) -- constructs products
| e . l | e . r --
New rules for products (Statics)
G |- e1 : t1 G |- e2 : t2
----------------------------------- (A)
G |- (e1,e2) : t1 * t2
G |- e : t1 * t2 G |- e : t1 * t2
---------------- ----------------
G |- e.l : t1 G |- e.r : t2
Omar's question: why have unit in your programming language? Why did Bob include them in this chapter?
(Dynamics, strict semantics)
e1 -> e1'
--------
(e1, e2) -> (e1', e2)
e1 val e2 -> e2'
---------------------
(e1, e2) -> (e1, e2')
(e1,e2) val
--------------------
(e1,e2).l -> e1
(e1,e2) val
--------------------
(e1,e2).r -> e2
e1 val e2 val
-------------------
(e1, e2) val
[Progress] 1. If empty |- e : t then either e is a value or there exists e', such that e -> e'
[Preservation] 2. If G |- e : t and e -> e', then G |- e' : t
Proofs are by structural induction. Example of preservation proof:
By induction on the stepping relation.
Example Case:
e1 -> e1'
---------------------
(e1, e2) -> (e1', e2)
Assume (e1,e2) : t and that the above stepping rule applies.
We want to show that (e1', e2) : t.
By inversion of rule (A), we know that t must be some t1 * t2, where
e1 : t1 and e2 : t2.
By induction hypothesis, we know that e1' : t1.
By rule (A) we know that (e1', e2) : t1 * t2.
Example of progress proof:
By induction on the typing relation
e1 : t1 e2 : t2
-------------------
(e1,e2) : t1 * t2
If e1 is a value then either e2 is a value or not.
If e2 is a velue then the tuple is a velu
If e2 is not a value, then tuple steps to (e1,e2')
If e1 is not a value, then tuple steps to (e1',e2)
Generalization to n-ary products
Hengchu: We can build n-ary products out of binary products by nesting them. Why would you choose one version of products over another.
See PrimRec.v
Rec defines iteration just by forgetting the extra argument
let G be fun f => fun m => fun r => f r
define:
iter' A n z f = rec A n z (G f)
We can also define the opposite direction. See PrimRec file, plus proof of equivalence of the versions.
-
I don’t understand why unit value should be considered a product.
[ SCw: This part of the chapter is talking about products with n-ary components. For example, we can think about not just pairs
(1, True) :: (Int, Bool)
but triples
(1, True, 'a') :: (Int, Bool, Char)
and so on
(1, True, 'a', "hello") :: (Int, Bool, Char, String)
In general, a product can have n-components. What if n is zero? Then we have unit.
() :: ()
-
I see that Ch10 is using product and tuple to define the types and expressions, in which the indexes are natural numbers. Is it possible that we use lists instead?
[ SCW: We can use any type that we want for indices, including natural numbers and string (i.e. labels, field names). Lists would also work, but are not standard.]
-
It would be good if the content of 10.3 could be covered and linked to the contents of ch9.
[SCW: Solomon plans to cover this]
-
What does it mean that using product types may simplify the primitive recursion construct of T? Is that because we get rid of a variable
yin the definition of recursion? Will this also simplify the construct in Coq?[ SCW: It actually gets rid of the variable 'x', the predecessor, in the definition of the recursor. It will also simplify the construct in Coq because there are fewer parts to the operator. ]
-
Ch 8 begins like 'In the language E, we may perform calculations such as the doubling of a given expression, but we cannot express doubling as a concept in itself.' We could overcome this problem by adding function types. Now the question is, what have we gained by adding product types? More specifically, has the language become more expressive? Section 10.3 states that 'Using products we may simplify the primitive recursive construct of T ...'. So one advantage of adding product types is simplicity. Section 10.3 further discusses mutual primitive recursion. Is it impossible to implement mutual primitive recursion without product types? If not, what else have we gained other than simplicity?
[SCW: good question. The answer depends on what you mean by "expressivity". If you are willing to do a whole-program transformation, it may be possible to implement primitive recursion without product types. I'll have to think about it.]
-
I am wondering if all mutual recursions with n mutually recursive functions can be encoded with n-tuple types? Does that mean there is really no need to for any built-in semantics of mutual recursion for languages that we are developing?
[ SCW: Solomon plans to cover this. ]
- In section 10.3, I wasn't sure if there was meant to be an implicit subtyping relationship in the discussion of typing products? If there are multiple different types with index sets that share some indices, does rule 10.3b mean we can use a value of any of those in the place of e?
[SCW: Yes. If we have two different record types that share labels, then 10.3b applies to both.
type T1 = { l :: Int, k :: Char }
type T2 = { l :: Bool, j :: String }
Then the expression \x -> x.l can be given type T1 -> Int OR T2 -> Bool OR { l :: Int } -> Int OR { l :: Bool } -> Bool.
But this is not really subtyping as there is no declared relationship between types. ]
-
After reading ch 10, I am wondering the case where the types of latter elements depend on the value of former elements. In this case, what should be changed for the static and dynamic rules? Does it mean that we need to evaluate the value according to the index order?
[SCW: For the first question, see dependent types. In that case, the binary product is written "Sigma x:tau1. tau2" so that tau2 can mention x, the value of first component. The typing rule requires a substitution when typing the second component:
G |- e1 : tau1 G |- e2 : tau2 { e1 / x } ----------------------------------------------- G |- < e1, e2 > : Sigma x:tau1. tau2There are two different elimination forms for Sigma types. The weak form uses pattern matching:
G |- e1 : Sigma x:tau1. tau2 G, x:tau1, y:tau2 |- e2 : tau G |- tau ok (make sure x and y don't escape in tau) ----------------------------------- G |- let (x, y) = e1 in e2 : tauThe stronger form uses projections:
G |- e : Sigma x:tau1. tau2 G |- e : Sigma x:tau1. tau2
G |- fst e : tau1 G |- snd e : tau2 { fst e / x }As far as dynamics goes, things are best when <e1,e2> is nonstrict (i.e. doesn't evaluate either argument). ]
-
The book states that the fixpoint operator allows us to solve "any set of recursion equations we like", which seems to suggest that any set of recursion equations has an associated functional. But there should be conditions on these equations:
-
E.g. f(0) = 0, f(n + 1) = 0 and f(n + 1) = 1 is an inconsistent system of recursion equations.
-
E.g. It's not clear what functional an equation like f(f(n + 1)) = f(f(n)) has.
The book probably just means defining equations in the form given in the factorial example, but something like f(n + 2) = f(n + 1) + f(n), f(0) = 1 = f(1) should work too (?).
[SCW: Not sure what part of the book you are referring to. You are right that there are sets of equations with no solution; i.e. that do not define mathematical functions.]
-
================================