<jupyter_start><jupyter_text>Definite article tutorial Authors: <NAME>, <NAME>This notebook goes through what is involved in adding a new variable-binding operator to the metalanguage and instantiating it in a lexical entry, by working through iota.<jupyter_code>#reload_lamb() # can be uncommented for debugging purposes (this will reload any changes made to the source files)<jupyter_output><empty_output><jupyter_text>This notebook walks through the process of adding a new operator, iota, to the lambda notebook.The notebook has two main parts: the metalanguage, and the object language.  To add iota, we need to modify the meta-language, and then using it in the object language is straightforward.Every expression in the metalanguage is represented by an object that inherits from the class _TypedExpr_.  Operators that bind a single variable and have a nuclear scope inherit from the subclass _BindingOp_, for example _ExistsUnary_ and _ForallUnary_.  To add Iota, we also subclass from _BindingOp_.  This basically involves specifying type constraints for the variable, the body, and the entire expression.  The default is that the body type and overal type are the same, but this is wrong for iota.  For iota, the body type is type t, and the variable / output type are equal.  A stricter version of this might enforce that both are type e.To add this to the parser, I also added a hook in the function _TypedExpr.try_parse_op_expr_ in meta.py.  (In the future this should happen more automatically.)<jupyter_code># note: IotaUnary has been added to meta.py, parallel code here for exemplification.
class DemoIotaUnary(meta.BindingOp):
    canonical_name = "Iota" # set the token for parsing this operator
    op_name_uni = "ι"
    op_name_latex = "\\iota{}"
    secondary_names = {"ι"}
    
    def __init__(self, var_or_vtype, body, varname=None, assignment=None, type_check=True):
        super().__init__(var_or_vtype=var_or_vtype, typ=None, varname=varname, body=body, body_type=types.type_t, assignment=assignment, type_check=type_check)
        self.type = self.vartype # output type is the bound variable's type

    def copy(self):
        return DemoIotaUnary(self.vartype, self.body, varname=self.varname)
    
    def copy_local(self, var, arg, type_check=True):
        return DemoIotaUnary(var, arg, type_check=type_check)

meta.BindingOp.add_op(DemoIotaUnary) # add to the registry of binding operators so that it will be parsed.  This will trigger a warning as it overrides the existing IotaUnary class.<jupyter_output><empty_output><jupyter_text>The following examples demonstrate instantiating this class through python class constructions.  (Recall that _lang.te_ calls the metalanguage parser.)<jupyter_code>test = DemoIotaUnary("x_e", lang.te("P(x)"))
test
test2 = meta.LFun("f_<e,t>", DemoIotaUnary("x_e", lang.te("f_<e,t>(x_e)")))
test2<jupyter_output><empty_output><jupyter_text>The following cells demonstrate instatiating iota via the metalanguage parser, and test out combining it with a property.<jupyter_code>the = lang.te("L f_<e,t> : Iota x_e : f(x)")
the
%%lamb
catexpr = L x_e : Cat(x) # build a property 'catexpr'
dp = the(catexpr)
dp
dp.reduce()
dp.reduce_all()
dp.reduce_all().derivation<jupyter_output><empty_output><jupyter_text>It's worth checking that the type inference is working correctly.  What happens when something not of type t is supplied as the body?  Is the output type right?The following code catches and displays a TypeMismatch if any.  (To see the full stack trace, you can remove the `try...except` part.)<jupyter_code>result = None
try:
    lang.te("Iota x_e : x")
except types.TypeMismatch as e:
    result = e
result
lang.te("Iota x_e : P(x)").type
lang.te("Iota x_e : P(x)").__class__
# another way of constructing this:
#test3 = lang.te("P_<e,t>")(lang.te("Iota x_e : Q(x)"))
test3 = lang.te("P_<e,t>(Iota x_e : Q(x))")
test3
test3.type<jupyter_output><empty_output><jupyter_text>Now let's use this in a lexical item.  With the metalanguage modifications in place, this is straightforward.<jupyter_code>%%lamb
||the|| = L f_<e,t> : Iota x_e : f(x)
||cat|| = L x_e : Cat(x)
r = the * cat
r.reduce_all()
r
r.tree(derivations=True)<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.09105960264900662, 'fraction_numerical': 0.0014191106906338694, 'mean_word_length': 5.155749636098981, 'pattern_counts': {'":': 0, '<': 33, '<?xml version=': 0, '>': 33, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '6', 'dir': 'jupyter-structured-clean-dedup', 'id': '488440', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 1365, 'n_tokens_neox': 1337, 'n_words': 491, 'path': 'notebooks/tutorials/definite article tutorial.ipynb', 'repo_name': 'poetaster-org/lambda-notebook', 'size': '4239'}