Mentions légales du service

Skip to content
  • Andrei Paskevich's avatar
    Term: lambda-manipulating functions · 235fac91
    Andrei Paskevich authored
    Two points for discussion:
    
    - t_lambda accepts both terms and formulas for the body.
      Thus, t_open_lambda, t_app_lambda, and t_app_beta can all
      return a term or a formula, depending on what is inside
      the lambda term. The caller should not forget to check.
      We could, in principle, always return a term (bool-typed
      when needed), which would exclude a possible run-time error,
      but then a caller who expects a formula, would have to
      recognize the results of the form [if f then True else False],
      before blindly attaching [== True] to them. Maybe still worth it:
      it's better if a forgotten check leads to an inefficient formula
      than to a type-checking error.
    
    - t_lambda takes a preid which will be the binding variable in the
      produced epsilon. This permits us to give names to our lambdas
      if we want it (what for?) and to give locations to intermediate
      terms inside the epsilon. Overall, it's not very useful and can
      probably be removed.
    235fac91