v0.8.0: Metasemantics

Release version available via PyPI: pip install lambda-notebook.

This version involves a major metalanguage/type system update, centered around
a new approach to metasemantics. This is probably the biggest set of changes
since the initial release.

New features:

• Meta-meta-language features (new module, lamb.meta.meta):
  • MetaTerm: this is a major change/improvement to how constant values
    (e.g. True) work. A MetaTerm is a direct, immutable reference to
    a backing python object that provides a metasemantics for the term. This
    change goes together with an explicit implementation of domain sets of
    python objects, providing backing domains for all simple types (e.g.
    type e is backed by strings of a certain kind, SetType is backed by
    python sets, functions are backed by mappings/callables, etc).
  • Simplification guarantees complete simplification when dealing with
    MetaTerms. This change also allows simplification for quantified
    expressions with finite domains (by iterating over the type domain).
  • Evaluations: much richer support for truth-table-like batch evaluations
    of boolean expressions. truthtable is a handy wrapper function on this.
  • extract_boolean: given an arbitrary metalanguage expression, produce
    a purely boolean expression together with an assignment filling in the
    non-boolean parts.
  • An implementation of first-order model theory using the evaluation system.
• Metalanguage features
  • Set operations: intersection, union, difference. Core relations:
    equivalence, the various sub/superset relations.
  • Set-related simplification heuristics.
  • A ternary conditional operator Case
  • Operators Dom, Codom and Fun, as well as a sequencing operator
    + for working with functions.
  • A facade class for working with TypedExprs.
  • Improvements to operator handling, including the ability to define
    operators based on metalanguage functions.
  • Support for restricted quantification for existential and universal
    operators (and Iota).
• Type system features:
  • As noted above, the ontology for simple types is new essentially complete,
    at least for the finite case, by implementing domain sets.
  • Type domains allow domain restriction in order to work with finite
    examples. The easiest api for this is the context manager function
    restrict_domain on atomic types.
  • A new type constructor (∀) that unselectively binds type variables in its
    scope. This is only semi-intended to be user facing, as it isn't easy
    to understand. However, this directly supports the next feature:
  • Support for full let-polymorphism via assignments. That is, polymorphic
    functions in assignments can now have distinct specializations in the
    same expression (previously they would have to unify to a coherent type;
    let-polymorphism could only be achieved anonymously via reduction).
• Metalanguage "compilation": expressions with no free variables can now be
  converted to python code that runs roughly within an order of magnitude of
  similar code implemented directly in python. In many cases, this is much
  faster than simplification, and sometimes in a way that matters (especially
  with quantification in play). There are certain other caveats: finite sets
  only, equivalence of functions can't be dynamically determined.
• Simplification and expression manipulation features:
  • new module, lamb.meta.ply, hosts various code (new and old) for generic
    manipulation and introspection on TypedExpr objects.
  • term order normalization for n-ary operations where this is appropriate
    (e.g. &, |). This normalizes order and structure (to left commutivity).
    This approach allows keeping strict binary operators, but when
    appropriate, manipulating them as n-ary sequences.
  • more configurable simplification, with a number of options that may not
    be used by default. (Roughly building on SymPy's approach.) For example,
    the eliminate_sets option will convert set operations/relations to
    booleans where possible, though this may make formulas more complicated.
• Error / exception handling and display, especially in magic contexts, is
  rewritten. New context manager lamb.errors() allows clean handling of
  lambda notebook-specific errors.
• Composition:
  • compose order is now preserved and used in rendering for bottom-up
    composition.
  • composition objects now support a function source_tree(), which extracts
    an underlying nltk-style Tree for display.

Documentation and sample notebooks:

• New documentation for sets, meta-meta-language expressions
• Rewritten: Hamblin semantics fragment

Fixes, improvements, changes:

• types and related issues:
  • many internal improvements/changes to type inference. One thing to note is
    that internal type variables will now appear as ? followed by a number,
    rather than as I variables.
  • improvements to anonymous let-polymorphism, which was previously very
    non-general
  • Many bug fixes to do with polymorphism
• improvements to simplification with recursive Tuple expressions
• improvements to inference for Partial expressions.
• improvements to derivations. The most public-facing change is that
  derivation reasons are now visually aligned with the origin step, not the
  result step. These objects now better support introspection, as well.
• many improvements to metalanguage simplification and reduction heuristics.
• improvements to latex rendering compatibility, including colab (katex) and
  mathjax 3.
• Older support code has been removed