Logical Notations🔗ℹ

Cameron Moy

Ryan Jung

This library provides a number of domain-specific DSLs, especially suited from writing domain-specific contracts.

1 Match🔗ℹ

syntax
(match e [pat e ...+] ...)

pat = id
| (var id)
| (and2 pat pat)
| (? expr)
| (app expr pat)
| (struct-id pat ...)
| (not pat)

A match pattern language, similar to Racket’s.

> (struct foo (x y))
> (match (foo 1 2)
[(foo z w) (+ z w)])
3

syntax
(define-match-expander id body)

Defines a match pattern macro, similar to Racket’s match expander.

2 Past-Time Linear Temporal Logic (PLTL)🔗ℹ

(require logic/pltl)

package: logic-lib

syntax
(define-pltl id ϕ)

ϕ = (neg ϕ)
| (disj ϕ ϕ)
| (conj ϕ ϕ)
| (exists (id ...) ϕ)
| (previous ϕ)
| (since ϕ ϕ)
| pat

Defines a PLTL formula that can be used in pltl. PLTL formulae must be monitorable, otherwise a compile-time error is raised. Atomic propositions are match patterns.

syntax
(neg e)
Represents the negation of formula e. A negation can only appear inside a formula of the following shapes: (conj a (neg b)), (conj (neg a) b), (since (neg a) b).

syntax
(disj l r)
Represents the disjunction of two formulae. The free variables of l must be equal to the free variables of r.

syntax
(conj l r)
Represents the conjunction of two formulae. There is a restriction on conjunctions of the following shapes: (conj (neg a) b), (conj b (neg a)). Namely, the free variables of a must be a subset of the free variables of b.

syntax
(exists (x ...+) e)
Given the a sequence of variables, this formula is satisfied when there exists some mapping from the variables to values such that e holds. The free variables of the entire formula is the set of free variables of e minus the quantified xs.

syntax
(previous e)
Requires that e be satisfied at the last time step.

syntax
(since l r)
Requires that there is some time in the past such that r holds. Since the latest such time (inclusive) until the current time step (exclusive), l holds. The free variables of l must be a subset of the free variables of r.

syntax
(define-pltl-rule (name arg ...) body)

Defines a PLTL macro.

syntax
(pltl formula)

Compiles a PLTL formula into a machine.

> (machine-accepts? (pltl (previous (? number?))) '(1 a))
#t
> (machine-accepts? (pltl (previous (? number?))) '(1 a 2))
#f

3 Regular Expressions (RE)🔗ℹ

(require logic/re)

package: logic-lib

syntax
(define-re id r)

r = (complement r)
| (seq r ...)
| (union r ...)
| (star r)
| (epsilon)
| (nullset)
| pat

Defines a regular expression that can be used in re.

syntax
(complement r)
Returns the complement of r, i.e., everything accepted by r is no longer accepted and vice versa.

syntax
(seq r ...)
Returns the concatenation of the given regular expressions.

syntax
(union r ...)
Returns the union of the given regular expressions.

syntax
(star r)
Returns the Kleene star, i.e. zero or more repetitions, of the given regular expression.

syntax
(epsilon)
A regular expression corresponding to the singleton language with the empty string.

syntax
(nullset)
A regular expression corresponding to the empty language.

syntax
(define-re-rule name body)
(define-re-rule (name arg ...) body)

Defines a regular expression macro.

syntax
(re r)

Compiles a regular expression into a machine.

> (machine-accepts? (re (plus 'a)) '(a a))
#t
> (machine-accepts? (re (plus 'a)) '(a b))
#f

4 Deterministic Finite Automata (DFA)🔗ℹ

(require logic/dfa)

package: logic-lib

syntax
(dfa start
(accept ...)
[state evt next-state] ...)

Compiles the given DFA to a machine.

> (define M
    (dfa s1 (s1)
         [s1 (equal? 0) s2]
         [s1 (? even?) s1]
         [s2 (equal? 0) s1]
         [s2 (? even?) s2]))
> (machine-accepts? M (list 2 0 4 0 2))
#t
> (machine-accepts? M (list 0 4 0 2 0))
#f

5 Non-deterministic Finite Automata (NFA)🔗ℹ

(require logic/nfa)

package: logic-lib

syntax
(nfa start
(accept ...)
[state evt next-state] ...)

Compiles the given NFA to a machine.

6 Quantified Event Automata (QEA)🔗ℹ

(require logic/qea)

package: logic-lib

syntax
(qea opt ...)

opt = (∀ id)
| (∃ id)
| (start id)
| (field fld-id expr)
| [-> src-id pat tgt-id trans-opt ...]

trans-opt = (when expr)
| (set fld-id expr)

Compiles the given QEA to a machine.

> (define Q
    (qea
      (∀ i)
      (start start)
      (field curr-bid 0)
      (field min-bid 0)
      [-> start (list 'put-up-item i r) item-listed
          (set curr-bid 0)
          (set min-bid r)]
      [-> item-listed (list 'bid i a) item-listed
          (when (> a curr-bid))
          (set curr-bid a)]
      [-> item-listed (list 'sell i) sold
          (when (> curr-bid min-bid))]))
> (machine-accepts? Q '((put-up-item a 10)
                        (put-up-item b 50)
                        (bid a 100)
                        (sell a)))
#t
> (machine-accepts? Q '((put-up-item a 10)
                        (put-up-item b 50)
                        (bid a 5)
                        (sell a)))
#f

syntax
(∀ id)
Universally quantifies the machine over id.

syntax
(∃ id)
Existentially quantifies the machine over id.

syntax
(start id)
Specifies the start state of the QEA.

syntax
(field id)
Specifies a field of the QEA.

syntax
[-> src-id pat tgt-id trans-opt ...]
Specifies a transition of the QEA.

syntax
(when expr)
The transition can only occur when expr is #t, where expr can reference fields.

syntax
(set fld-id expr)
Sets the given field when the transition it taken.

7 Stream Logic (SL)🔗ℹ

(require logic/sl)

package: logic-lib

syntax
(sl (id ...) [id expr] ...)

Compiles the given set of stream logic equations to a machine.

> (define S
    (sl
      (in)
      [out (and (out -1 #t) (set-first in))]))
> (machine-accepts? S '((in . #t) (in . #t) (in . #t)))
#t
> (machine-accepts? S '((in . #t) (in . #t) (in . #f)))
#f

1	Match
2	Past-Time Linear Temporal Logic (PLTL)
3	Regular Expressions (RE)
4	Deterministic Finite Automata (DFA)
5	Non-deterministic Finite Automata (NFA)
6	Quantified Event Automata (QEA)
7	Stream Logic (SL)