|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | + |
| 4 | += PolyglotFormalisms.Elixir |
| 5 | +:toc: preamble |
| 6 | +:icons: font |
| 7 | + |
| 8 | +Elixir implementation of the PolyglotFormalisms Common Library specification. |
| 9 | + |
| 10 | +== Overview |
| 11 | + |
| 12 | +This package provides Elixir implementations of fundamental operations defined |
| 13 | +in the PolyglotFormalisms specification, enabling semantic equivalence |
| 14 | +verification across multiple programming languages. |
| 15 | + |
| 16 | +== Modules |
| 17 | + |
| 18 | +=== Arithmetic |
| 19 | + |
| 20 | +* `add(a, b)` — Addition |
| 21 | +* `subtract(a, b)` — Subtraction |
| 22 | +* `multiply(a, b)` — Multiplication |
| 23 | +* `divide(a, b)` — Division |
| 24 | +* `modulo(a, b)` — Modulo (integer operation) |
| 25 | + |
| 26 | +=== Comparison |
| 27 | + |
| 28 | +* `less_than(a, b)` — Strict less than |
| 29 | +* `greater_than(a, b)` — Strict greater than |
| 30 | +* `equal(a, b)` — Equality |
| 31 | +* `not_equal(a, b)` — Inequality |
| 32 | +* `less_equal(a, b)` — Less than or equal |
| 33 | +* `greater_equal(a, b)` — Greater than or equal |
| 34 | + |
| 35 | +=== Logical |
| 36 | + |
| 37 | +* `logical_and(a, b)` — Logical conjunction |
| 38 | +* `logical_or(a, b)` — Logical disjunction |
| 39 | +* `logical_not(a)` — Logical negation |
| 40 | + |
| 41 | +NOTE: Function names include `logical_` prefix to avoid conflicts with Elixir's Kernel reserved keywords. |
| 42 | + |
| 43 | +== Installation |
| 44 | + |
| 45 | +[source,elixir] |
| 46 | +---- |
| 47 | +def deps do |
| 48 | + [ |
| 49 | + {:polyglot_formalisms, "~> 0.2.0"} |
| 50 | + ] |
| 51 | +end |
| 52 | +---- |
| 53 | + |
| 54 | +== Usage |
| 55 | + |
| 56 | +[source,elixir] |
| 57 | +---- |
| 58 | +alias PolyglotFormalisms.{Arithmetic, Comparison, Logical} |
| 59 | +
|
| 60 | +sum = Arithmetic.add(2.0, 3.0) |
| 61 | +product = Arithmetic.multiply(4.0, 5.0) |
| 62 | +is_less = Comparison.less_than(2.0, 3.0) |
| 63 | +is_equal = Comparison.equal(5.0, 5.0) |
| 64 | +both_true = Logical.logical_and(true, true) |
| 65 | +either_true = Logical.logical_or(false, true) |
| 66 | +negated = Logical.logical_not(false) |
| 67 | +---- |
| 68 | + |
| 69 | +== Mathematical Properties |
| 70 | + |
| 71 | +=== Arithmetic Properties |
| 72 | + |
| 73 | +* Commutativity (for add, multiply) |
| 74 | +* Associativity (for add, multiply) |
| 75 | +* Identity elements |
| 76 | +* Distributivity |
| 77 | + |
| 78 | +=== Comparison Properties |
| 79 | + |
| 80 | +* Transitivity |
| 81 | +* Reflexivity |
| 82 | +* Symmetry |
| 83 | +* Asymmetry |
| 84 | + |
| 85 | +=== Logical Properties |
| 86 | + |
| 87 | +* Commutativity |
| 88 | +* Associativity |
| 89 | +* Distributivity |
| 90 | +* De Morgan's laws |
| 91 | +* Excluded middle |
| 92 | +* Non-contradiction |
| 93 | + |
| 94 | +== Behavioral Semantics |
| 95 | + |
| 96 | +=== Float Operations |
| 97 | + |
| 98 | +* Division by zero returns `Infinity` or `-Infinity` |
| 99 | +* NaN propagation follows IEEE 754 |
| 100 | +* Comparison with NaN returns `false` |
| 101 | + |
| 102 | +=== Integer Operations |
| 103 | + |
| 104 | +* Modulo uses Erlang `rem` operator semantics |
| 105 | +* Modulo by zero raises `ArithmeticError` (BEAM behavior) |
| 106 | + |
| 107 | +=== Boolean Operations |
| 108 | + |
| 109 | +* Short-circuit evaluation for `and` and `or` |
| 110 | +* Eager evaluation for wrapper functions |
| 111 | + |
| 112 | +== Testing |
| 113 | + |
| 114 | +[source,bash] |
| 115 | +---- |
| 116 | +mix test |
| 117 | +mix test --include doctest |
| 118 | +---- |
| 119 | + |
| 120 | +== Cross-Language Verification |
| 121 | + |
| 122 | +This Elixir implementation is semantically equivalent to: |
| 123 | + |
| 124 | +* Julia implementation (PolyglotFormalisms.jl) |
| 125 | +* ReScript implementation (alib-for-rescript) |
| 126 | +* Gleam implementation (polyglot_formalisms_gleam) |
| 127 | + |
| 128 | +Formal verification proofs demonstrating semantic equivalence are available in |
| 129 | +the main PolyglotFormalisms specification repository. |
| 130 | + |
| 131 | +== Documentation |
| 132 | + |
| 133 | +[source,bash] |
| 134 | +---- |
| 135 | +mix docs |
| 136 | +---- |
| 137 | + |
| 138 | +== Architecture |
| 139 | + |
| 140 | +See link:TOPOLOGY.md[TOPOLOGY.md] for a visual architecture map and completion dashboard. |
| 141 | + |
| 142 | +== Related Projects |
| 143 | + |
| 144 | +* https://github.com/hyperpolymath/PolyglotFormalisms.jl[PolyglotFormalisms.jl] — Julia reference implementation |
| 145 | +* https://github.com/hyperpolymath/alib-for-rescript[alib-for-rescript] — ReScript implementation |
| 146 | +* https://github.com/hyperpolymath/polyglot_formalisms_gleam[polyglot_formalisms_gleam] — Gleam implementation |
| 147 | + |
| 148 | +Wondering how this works? See link:EXPLAINME.adoc[]. |
| 149 | + |
| 150 | +== License |
| 151 | + |
| 152 | +SPDX-License-Identifier: PMPL-1.0-or-later + |
| 153 | +See link:LICENSE[LICENSE]. |
0 commit comments