• generate
• prune a lot
• sample the values of conjectures based on the closest “unsolved” parts

There is a Self-Printing Turing Machine

Q

There’s a computable function \(q: \Sigma^{*} \to \Sigma ^{*}\) such that for every string \(w\), the computation \(q(w)\) produces the description of a Turing machine \(P_{w}\) such that on every input, it spits out \(w\) and then accepts.

B

For some turing machine code \(m\) making TM \(M\), the computable function \(B\) composes \(P_{m}\) from above and \(M\) (that is, the composition of \(P_{m}\) and \(M\) first disregards it input, prints \(m\), and give it to \(M\)).

The principle of semantic accountability claims that a good grammar should be able to say “something explicit about how the abstractions of the grammar match with actual meaning”

lower things into LLVM IR, HLO, etc. — “analyze the sentences”

• check type
• catch inconsistency
• scoping rules, etc.

Typical, we implement multiple passes for this because optimizing for multiple passes is quite hard. We need this because most grammars are not actually context free (for instance, scoping).

what to check

1. declaration of identifiers
2. types
3. inheritance relationships
4. class efined once
5. methods in a class defined only once
6. reserved identifiers are not misused (i.e., inherits, etc.)

example

type errors

let y: String <- "abc" in y+3

variables that don’t exist

let y : Int in x + 3

scope

the scope of an identifier is the portion of a program in which a particular identifier is accessible.

Represent health information in terms of rule-based ontologies.