Transcript NummSquared Coercion

NummSquared Coercion
make it so!
Samuel Howse
poohbist.com
[email protected]
November 29, 2006
Copyright © 2006 Samuel Howse. All rights
reserved.
Type theory
• Types can ensure termination and avoid paradoxes.
• But more complex – 2 fundamental concepts:
– Type
– Function
• Compile-time type checking is computable.
– Benefit – catch some bugs early and automatically
– Cost – additional constraints on programmer
• my research addresses by using runtime coercion instead of
compile-time type checking
• Coq proof assistant
– nice mix of computation and proof checking
– practical tools, including extraction to OCaml
– highly developed
Set theory
• Everything is a set.
• Well-founded set theory
– Membership (ε) is well-founded, i.e. no
infinite descending ε chains.
– A set is formed “after” its elements.
• Some well-founded set theories:
– Zermelo Fraenkel (ZF)
– von Neumann-Bernays-Gödel (NBG)
• Usually no reduction (computation)
Well-founded functions
• Everything is a function.
• Well-founded
– A function is formed “after” elements of its domain
and range. [Jones]
– Membership in field of function a well-founded
relation
• Few foundations of this kind, and not popular
• von Neumann in 1925
– Others changed functions to sets – became NBG
• Jones’s Pure Functions in 1998
• von Neumann and Jones – do not define
reduction (computation) or proof
NummSquared
• Everything a function, no types, no side-effects, no
global state, well-founded
• Reduction (computation) and proof
• Sound: the proposition of a valid proof is true
• Termination ensured without proofs by programmer
• Proofs as desired, but not required
• Classical logic
• Follows set theory as much as possible
• Simple variable-free syntax
• Reflection
– NummSquared is its own macro language.
– NummSquared is used to manipulate NummSquared proofs.
Domain membership
• When calling a function, how to ensure that
the argument belongs to the function’s
domain?
• Unrestricted domain – untyped lambda
calculus – non-termination
• Type constraints on programmer
• Set theory: higher-order domain membership
not computable – need proofs by
programmer
• NummSquared: coercion
•
•
•
•
NummSquared coercion for domain
membership
NummSquared coercion: if it isn’t so,
then make it so!
Type conversion generalized to higherorder (function with function argument)
Coerce a function to domain/codomain
by applying pre-coercion/post-coercion.
NummSquared coercion somewhat
related to Howe’s restriction of untyped
lambda terms.
– Howe does not ensure termination.
Semantics: small function extensions
simple
leaf
pair p
null (base case)
null
null
null<null>
= null
zero
p<null>
= null
zero
p<zero>
= left(p)
null
zero<null>
= null
one
null
rule f
x
zero
one<null> one<zero>
= null
= zero
…
dom(f)
f<x>
small
(no larger
than a ZFC set)
one
p<one>
= right(p)
Semantics: small function extensions
• Well-founded to ensure termination and avoid
paradoxes
• Defined inductively
• Rule f with:
– dom(f) a small set of small function extensions
• Small means no larger than a ZF set.
– for x in dom(f), f<x> is a small function extension
• Leaf: null, zero, one
– null means absence of relevant information – does not mean
0, false, undefined or non-termination
• Pair p such that left(p) and right(p) are small function
extensions
• A tree is a small function extension recursively
containing only leaves and pairs.
Semantics: domain extensions
• For a rule f, dom(f) is not, in general, amenable to coercion.
• So dom(f) represented by domain extension (tag):
– Same information as a type in type theory
– Different purpose – not compile-time type checking, but
runtime coercion
– Domain extensions never appear directly in NummSquared
programs, but are available as small function extensions.
• Domain extension:
– Constant: Dom.Null, Dom.Nuro (Null or Zero), Dom.Leaf,
Dom.Tree
– Combination: dependent sum/product A with domExtFam(A)
a domain extension family
• Domain extension family F with:
– dom(F) a small set of small function extensions
– for x in dom(F), F<x> is a domain extension
– domExt(F) is a domain extension
Semantics: domain of domain
extensions
•
•
•
•
•
dom(Dom.Null) = Null = {null}.
dom(Dom.Nuro) = Nuro = {null, zero}.
dom(Dom.Leaf) = Leaf = {null, zero, one}.
dom(Tree) = Tree = set of all trees
For dependent sum A, dom(A) = set of null and all pairs
p such that:
– left(p) in dom(domExtFam(A))
– right(p) in dom(domExtFam(A)<left(p)>)
• For dependent product A, dom(A) = set of null and all
rules f such that:
– dom(f) = dom(domExtFam(A))
– for x in dom(f), f<x> in dom(domExtFam(A)<x>)
Semantics: Domain extension
irrelevance
• Domain extension f is valid iff, for each
domain extension family G contained,
directly or indirectly, in f:
– dom(domExt(G)) = dom(G)
• Domain extension irrelevance theorem: for
valid domain extensions A and B, if
dom(A) = dom(B), then A = B.
– A domain extension contains no more
information than the domain it represents.
Semantics: tagged small function extensions
• Tagging
– Constrain rules by domain extensions
– Somewhat analogous to runtime type information
• Defined inductively
• Tagged rule f with:
– dom(f) a small set of small function extensions
– for x in dom(f), f<x> is a tagged small function extension
– domExt(f) is a valid domain extension such that
dom(domExt(f)) = dom(f)
• Leaf: as before
• Tagged pair p such that left(p) and right(p) are
tagged small function extensions
Semantics: Untag and tagged
• For tagged small function extension f, untag(f) is
obtained by removing domain extensions from f.
• Tag irrelevance theorem: for tagged small function
extensions f and g, if untag(f) = untag(g), then f = g.
• For valid domain extension A, and f in dom(A), tagged(A,
f) is the tagged small function extension such that
untag(tagged(A, f)) = f.
• For valid domain extension family F, and x in dom(F),
tagged(F, x) = tagged(domExt(F), x).
• For tagged small function extension f, and dom(f)
element x, tagged(f, x) = tagged(domExt(f), x).
Semantics: coercion
• For valid domain extension A and tagged small
function extension f, coercion to A of f, denoted by
coer(A, f), is in dom(A).
• If A is a dependent sum, and f is a pair, coerce left(f)
first, then right(f).
– coer(A, f) is the pair p such that:
• left(p) = coer(domExt(domExtFam(A)), left(f))
• right(p) = coer(domExtFam(A)<left(p)>, right(f))
• If A is a dependent product, and f is a rule, add precoercion and post-coercion to f:
– coer(A, f) is the rule r such that:
• dom(r) = dom(domExtFam(A))
• For x in dom(r), r<x> = coer(domExtFam(A)<x>,
f<coer(domExt(f), tagged(domExtFam(A), x))>)
Semantics: result
• See NummSquared Explained for:
– The precise recursive definition of coercion
– Justification of that recursive definition by a
well-founded relation
• Use coercion to define tagged small function
extensions over all tagged small function
extensions
• For tagged small function extensions f and x,
f(x) = f<coer(domExt(f), x)>
• Coercion and result are computable and
always terminate.
Semantics: large function
extensions
• Abstract over all tagged small function
extensions
• f such that, for each tagged small
function extension x, f(x) is a tagged
small function extension
• A large function extension is also a
proposition extension:
– f is true iff, for each tagged small function
extension x, f(x) = one
Semantics: recursion
• Terminating recursion principle based on
structure of small function extensions
• For large function extensions start and step,
~r[start step] is the large function extension such
that, for each tagged small function extension x:
– if x = null, ~r[start step](x) = start(x)
– otherwise, ~r[start step](x) = step({rDom, rRan, x})
where:
• rDom is the tagged rule such that domExt(rDom) = domExt(x)
and, for y in dom(rDom), rDom<y> = ~r[start
step](tagged(rDom, y))
• rRan is the tagged rule such that domExt(rRan) = domExt(x)
and, for y in dom(rRan), rRan<y> = ~r[start
step](x(tagged(rDom, y)))
NummSquared syntax
• Variable-free
• Large functions
– Constants
– Combinations
• Proofs
– Axioms
– Inferences
• Reflection
–
–
–
–
Quoting and unquoting large functions
Quoting and unquoting proofs
The quoted representation is a tree.
Quoting is easy because NummSquared is variable-free.
• See NummSquared Explained for details.
The Future
• Thanks to Hugo Herbelin and Bruno Barras for
suggesting some directions for the future.
• Current recursion principle is like ε or ordinal recursion,
but well-founded recursion requires proof
– Solution: In well-founded recursion, the proof is irrelevant for
computation.
• Define/prove NummSquared within first order logic +
NBG axioms
• First order logic axioms for NummSquared
• Model typed languages within NummSquared
– NummSquared models (unlike set theory models) are
computational
References
• My PhD thesis, NummSquared 2006a0
Explained
– poohbist.com
• Other references are in the bibliography of
NummSquared Explained.
• Short paper: NummSquared: a New
Foundation for Formal Methods
– poohbist.com
• These slides
– poohbist.com