Turned in the marriage form today. If all goes well, I will have Frank and Bob as co-advisors.

Machine learning was cancelled today; Bobclass consisted of more stuff about dependent types. The homework for complexity theory was postponed, hooray. The proofs that primality is in NP and (NP \cap coNP implies polytime factoring) are still vexing me slightly. I think I have finally figured out the hint for the former, under the assumption that simply citing "Primes is in P" is considered bad form. Just need to exhibit a generator g of the multiplicative group Z_p/{0}, and prove it is a generator by computing g^(p-1) mod p (and checking that it's 1) and g^k mod p for every prime factor k of p-1 (and checking that they're not 1). I think this should imply that the group generated by g within the multiplicative monoid Z_p in fact has size p-1.

Got some groceries; eggs, milk, apple juice, bread, raisins, bologna, individually wrapped cheez-like substance, potato chips. I think my grocery-buying habits tend towards an equilibrium of buying exactly \$20 of food per trip.

Read through Frank's linear logic notes again to refresh my memory concerning cut elimination. It did not dispel my fear that it amounts to a small amount of cute magic making sure normal proofs correspond to cut-free sequent proofs, and natural deduction proofs correspond to sequent proofs followed by a big nasty n^2-case induction that you just have to slog through, n being the number of sequent rules.
• #### (no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• #### (no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…

• #### (no subject)

Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic