The Kitchin Research Group

Hy allows us to define functions with unicode names. Here we play around with this to define logical operators with the symbols you normally see in formal papers (i.e. the LaTeX symbols). I think in Python3 you can also define unicode names for functions. It definitely does not work for Python2.7 which we use here (although remarkably via Hy it does work).

First, we define the logical operators or, and, xor and not, and a few other interesting ones. In case it is not clear why a unicode representation of and is helpful, note there are three instances of the word and in the previous sentence, and only one is a logical operator! This is just some syntactical beauty, but it will shortly make for a different representation of code. We tangle this code block to logical_operators.hy.

(defn ∨ [a b] (or a b))

(defn ∧ [a b] (and a b))

(defn ⊕ [a b] (xor a b))

(defn ¬ [a] (not a))

(defn ∀ [x func]
  "(func x) is True for every x."
  (every? func x))

(defn ∃ [x func]
  "func(x) is true for at least one x."
  (some func x))

(defn ∃! [x func]
  "func(x) is true for exactly one x."
  (= 1 (len (list (filter func x)))))

Here is an example of using those operators. At the moment, we use the prefix notation of Lisp.

(import [logical_operators [*]])
(import [serialize [stringify]])

(defmacro show [body]
  `(do
    (print (.encode (.format "{0} = {1}" (stringify '~body) ~body) "utf-8"))))

(show (¬ True))
(show (∧ True False))
(show (∧ True True))
(show (∨ True False))
(show (∨ True True))
(show (⊕ True False))
(show (⊕ True True))
(show (⊕ False False))
(show (∀ [2 4 6] even?))
(show (∃ [2 3 4] odd?))
(show (∃! [2 3 4] odd?))
(show (∃! [2 3 5] odd?))

(¬ True) = False
(∧ True False) = False
(∧ True True) = True
(∨ True False) = True
(∨ True True) = True
(⊕ True False) = True
(⊕ True True) = False
(⊕ False False) = False
(∀ [2 4 6] is_even) = True
(∃ [2 3 4] is_odd) = True
(∃_bang [2 3 4] is_odd) = True
(∃_bang [2 3 5] is_odd) = False

Note the exclamation mark got expanded to _bang. It is evidently an ordinary ascii character.

We can get an infix notation if we use our infix module and the #$ reader macro defined in it. Here are some examples. Note it doesn't make sense to use this all time, e.g. it would even be a mistake to do this with the not operator.

(import [logical_operators [*]])
(import [serialize [stringify]])
(import [infix [*]])
(require infix)

(defmacro show [body]
  `(do
    (print (.encode (.format "{0} = {1}" (stringify '~body) ~body) "utf-8"))))

(show (¬ True))
(show #$(True ∧ False))
(show #$(True ∧ True))
(show #$(True ∨ False))
(show #$(True ∨ True))
(show #$(True ⊕ False))
(show #$(True ⊕ True))
(show #$(False ⊕ False))

(¬ True) = False
(dispatch_reader_macro "$" (True ∧ False)) = False
(dispatch_reader_macro "$" (True ∧ True)) = True
(dispatch_reader_macro "$" (True ∨ False)) = True
(dispatch_reader_macro "$" (True ∨ True)) = True
(dispatch_reader_macro "$" (True ⊕ False)) = True
(dispatch_reader_macro "$" (True ⊕ True)) = False
(dispatch_reader_macro "$" (False ⊕ False)) = False

The show macro shows us how the reader macro gets expanded into, you guessed it, regular old function calls. They are just syntactical sugar to help us be more concise. The unicode symbols are not quite as simple to type as ascii names, but there are solutions to this: abbreviations in Emacs (http://ergoemacs.org/emacs/emacs_n_unicode.html ), custom commands, learn the keystrokes (http://www.johndcook.com/blog/emacs_unicode/ ) and C-x 8 RET and the unicode name, etc… Is it worth it? That might depend on how ingrained those logical symbols are in your mental model of your work. If it is deeply ingrained, your code will be better aligned with your thoughts, and easier to understand.

Copyright (C) 2016 by John Kitchin. See the License for information about copying.

org-mode source

Org-mode version = 8.2.10