• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
        • Proof-support
        • Abstract-syntax
          • Syntax-abstraction
          • Expression
            • Expression-fix
            • Expression-case
            • Expressionp
            • Expression-count
            • Expression-equiv
            • Expression-mul
            • Expression-add
            • Expression-var
            • Expression-const
            • Expression-kind
          • Definition
          • Constraint
          • Definition-option
          • Abstract-syntax-operations
          • System
          • Convenience-constructors
          • System-result
          • Expression-result
          • Expression-list-result
          • Definition-result
          • Definition-list-result
          • Constraint-result
          • Constraint-list-result
          • Expression-list
          • Definition-list
          • Constraint-list
        • R1cs-subset
        • Semantics
        • Abstract-syntax-operations
        • Indexed-names
        • Well-formedness
        • Concrete-syntax
        • R1cs-bridge
        • Parser-interface
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Abstract-syntax

Expression

Fixtype of expressions.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:const → expression-const
:var → expression-var
:add → expression-add
:mul → expression-mul

We use any integers as constants. This way, the definition of expression (and of the other syntactic entities) does not depend on (the prime number that defines) the prime field. Semantically, integers are treated modulo the prime.

We use (any) strings for variables.

We include just two field operations for now: addition and multiplication. These suffice for arithmetic circuits. Negation, and therefore subtraction, are easily represented, via multiplication by negative one (see expression-neg and expression-sub). We may add other operations in the future, most notably reciprocal, and therefore division. We may also add square roots, and even support user defined functions. Some of these operations will introduce the issue of well-definedness, e.g. non-zero divisors.

Subtopics

Expression-fix
Fixing function for expression structures.
Expression-case
Case macro for the different kinds of expression structures.
Expressionp
Recognizer for expression structures.
Expression-count
Measure for recurring over expression structures.
Expression-equiv
Basic equivalence relation for expression structures.
Expression-mul
Expression-add
Expression-var
Expression-const
Expression-kind
Get the kind (tag) of a expression structure.