use super::functions::*;
pub struct HyperfiniteProb {
pub size: usize,
}
impl HyperfiniteProb {
pub fn new(size: usize) -> Self {
assert!(size > 0, "size must be positive");
HyperfiniteProb { size }
}
pub fn internal_prob(&self, set: &[usize]) -> f64 {
set.len() as f64 / self.size as f64
}
pub fn loeb_prob(&self, set: &[usize]) -> f64 {
self.internal_prob(set)
}
pub fn loeb_independent(&self, a: &[usize], b: &[usize]) -> bool {
let pa = self.loeb_prob(a);
let pb = self.loeb_prob(b);
let a_set: std::collections::HashSet<usize> = a.iter().cloned().collect();
let b_set: std::collections::HashSet<usize> = b.iter().cloned().collect();
let inter: Vec<usize> = a_set.intersection(&b_set).cloned().collect();
let pab = self.loeb_prob(&inter);
approx_equal(pab, pa * pb, 1e-10)
}
}
pub struct TransferPrinciple;
impl TransferPrinciple {
pub fn new() -> Self {
Self
}
pub fn first_order_statement_transfers(&self) -> bool {
true
}
pub fn internal_sets_transfer(&self) -> bool {
true
}
}
pub struct Hyperreal {
pub standard: f64,
pub infinitesimal_part: f64,
pub infinite_part: f64,
}
impl Hyperreal {
pub fn new(standard: f64, infinitesimal_part: f64, infinite_part: f64) -> Self {
Self {
standard,
infinitesimal_part,
infinite_part,
}
}
pub fn standard_part(&self) -> Option<f64> {
if self.is_finite() {
Some(self.standard)
} else {
None
}
}
pub fn is_finite(&self) -> bool {
self.infinite_part == 0.0
}
pub fn is_infinitesimal(&self) -> bool {
self.standard == 0.0 && self.infinite_part == 0.0
}
}
pub struct ModelTheoryConnection;
impl ModelTheoryConnection {
pub fn new() -> Self {
Self
}
pub fn ultrafilter_construction(&self) -> bool {
true
}
pub fn los_theorem(&self) -> bool {
true
}
}
pub struct InternalSet {
pub property: String,
}
impl InternalSet {
pub fn new(property: String) -> Self {
Self { property }
}
pub fn is_internal(&self) -> bool {
!self.property.is_empty()
}
pub fn overflow_principle(&self) -> bool {
true
}
}
pub struct NonStandardSequence {
pub terms: Vec<f64>,
}
impl NonStandardSequence {
pub fn new(terms: Vec<f64>) -> Self {
Self { terms }
}
pub fn st_convergence(&self) -> Option<f64> {
if self.terms.is_empty() {
return None;
}
let last = *self
.terms
.last()
.expect("non-empty vec always has a last element");
if last.is_finite() {
Some(last)
} else {
None
}
}
pub fn is_ns_cauchy(&self) -> bool {
if self.terms.len() < 2 {
return true;
}
let n = self.terms.len();
let diff = (self.terms[n - 1] - self.terms[n - 2]).abs();
diff < 1e-10
}
}
pub struct LoebMeasure {
pub hyperfinite_set: String,
}
impl LoebMeasure {
pub fn new(hyperfinite_set: String) -> Self {
Self { hyperfinite_set }
}
pub fn loeb_measure(&self) -> f64 {
if self.hyperfinite_set.is_empty() {
0.0
} else {
1.0
}
}
pub fn is_standard_measure(&self) -> bool {
true
}
}
#[derive(Debug, Clone)]
pub struct HyperrealApprox {
pub seq: Vec<f64>,
pub filter: PrincipalUltrafilter,
}
impl HyperrealApprox {
pub fn constant(r: f64, n: usize, principal: usize) -> Self {
HyperrealApprox {
seq: vec![r; n],
filter: PrincipalUltrafilter::new(n, principal),
}
}
pub fn from_seq(seq: Vec<f64>, principal: usize) -> Self {
let n = seq.len();
HyperrealApprox {
seq,
filter: PrincipalUltrafilter::new(n, principal),
}
}
pub fn value(&self) -> f64 {
self.seq[self.filter.principal]
}
pub fn is_standard_zero(&self) -> bool {
self.value().abs() < f64::EPSILON
}
pub fn standard_part(&self) -> f64 {
self.value()
}
pub fn add(&self, other: &Self) -> Self {
assert_eq!(self.seq.len(), other.seq.len(), "sequence length mismatch");
let seq: Vec<f64> = self
.seq
.iter()
.zip(other.seq.iter())
.map(|(a, b)| a + b)
.collect();
HyperrealApprox {
seq,
filter: self.filter.clone(),
}
}
pub fn mul(&self, other: &Self) -> Self {
assert_eq!(self.seq.len(), other.seq.len(), "sequence length mismatch");
let seq: Vec<f64> = self
.seq
.iter()
.zip(other.seq.iter())
.map(|(a, b)| a * b)
.collect();
HyperrealApprox {
seq,
filter: self.filter.clone(),
}
}
pub fn abs(&self) -> Self {
let seq: Vec<f64> = self.seq.iter().map(|x| x.abs()).collect();
HyperrealApprox {
seq,
filter: self.filter.clone(),
}
}
}
pub struct StandardPart {
pub hyperreal: f64,
}
impl StandardPart {
pub fn new(hyperreal: f64) -> Self {
Self { hyperreal }
}
pub fn st(&self) -> f64 {
self.hyperreal
}
pub fn is_defined(&self) -> bool {
self.hyperreal.is_finite()
}
}
#[allow(dead_code)]
pub struct InternalFunction {
pub grid: Vec<f64>,
pub values: Vec<f64>,
}
#[allow(dead_code)]
impl InternalFunction {
pub fn new(grid: Vec<f64>, values: Vec<f64>) -> Self {
assert_eq!(
grid.len(),
values.len(),
"grid and values must have the same length"
);
Self { grid, values }
}
pub fn from_fn<F: Fn(f64) -> f64>(grid: Vec<f64>, f: F) -> Self {
let values = grid.iter().map(|&x| f(x)).collect();
Self { grid, values }
}
pub fn eval_nearest(&self, x: f64) -> f64 {
if self.grid.is_empty() {
return f64::NAN;
}
let idx = self
.grid
.iter()
.enumerate()
.min_by(|(_, a), (_, b)| {
((*a - x).abs())
.partial_cmp(&((*b - x).abs()))
.unwrap_or(std::cmp::Ordering::Equal)
})
.map(|(i, _)| i)
.unwrap_or(0);
self.values[idx]
}
pub fn ns_derivative_at(&self, i: usize) -> f64 {
if i + 1 >= self.grid.len() {
return 0.0;
}
let dx = self.grid[i + 1] - self.grid[i];
if dx.abs() < f64::EPSILON {
return 0.0;
}
(self.values[i + 1] - self.values[i]) / dx
}
pub fn riemann_sum(&self) -> f64 {
let n = self.grid.len();
if n < 2 {
return 0.0;
}
(0..n - 1)
.map(|i| self.values[i] * (self.grid[i + 1] - self.grid[i]))
.sum()
}
}
#[allow(dead_code)]
pub struct HyperfiniteSet {
pub cardinality: usize,
pub label: String,
}
#[allow(dead_code)]
impl HyperfiniteSet {
pub fn new(cardinality: usize, label: &str) -> Self {
Self {
cardinality,
label: label.to_string(),
}
}
pub fn hyperfinite_sum<F: Fn(usize) -> f64>(&self, f: F) -> f64 {
(0..self.cardinality).map(|k| f(k)).sum()
}
pub fn hyperfinite_product<F: Fn(usize) -> f64>(&self, f: F) -> f64 {
(0..self.cardinality).map(|k| f(k)).product()
}
pub fn loeb_integral<F: Fn(usize) -> f64>(&self, f: F) -> f64 {
if self.cardinality == 0 {
return 0.0;
}
self.hyperfinite_sum(f) / self.cardinality as f64
}
pub fn is_nonempty(&self) -> bool {
self.cardinality > 0
}
}
#[derive(Debug, Clone)]
pub struct PrincipalUltrafilter {
pub index_size: usize,
pub principal: usize,
}
impl PrincipalUltrafilter {
pub fn new(index_size: usize, element: usize) -> Self {
assert!(element < index_size, "principal element out of range");
PrincipalUltrafilter {
index_size,
principal: element,
}
}
pub fn contains_set(&self, set_mask: u64) -> bool {
(set_mask >> self.principal) & 1 == 1
}
pub fn is_free(&self) -> bool {
false
}
}
pub struct InfinitesimalCalculus;
impl InfinitesimalCalculus {
pub fn new() -> Self {
Self
}
pub fn derivative_as_ratio(&self) -> bool {
true
}
pub fn integral_as_sum(&self) -> bool {
true
}
pub fn is_rigorous(&self) -> bool {
true
}
}
#[allow(dead_code)]
pub struct HyperrealMonad {
pub center: f64,
pub epsilon: f64,
}
#[allow(dead_code)]
impl HyperrealMonad {
pub fn new(center: f64, epsilon: f64) -> Self {
Self { center, epsilon }
}
pub fn contains(&self, x: f64) -> bool {
(x - self.center).abs() < self.epsilon
}
pub fn widen(&self, factor: f64) -> Self {
Self {
center: self.center,
epsilon: self.epsilon * factor,
}
}
pub fn standard_part(&self, x: f64) -> Option<f64> {
if self.contains(x) {
Some(self.center)
} else {
None
}
}
pub fn overlaps(&self, other: &Self) -> bool {
(self.center - other.center).abs() < self.epsilon + other.epsilon
}
}
pub struct NSIntegral {
pub f: String,
pub a: f64,
pub b: f64,
}
impl NSIntegral {
pub fn new(f: String, a: f64, b: f64) -> Self {
Self { f, a, b }
}
pub fn riemann_integral_via_ns(&self) -> f64 {
let n = 1_000_000usize;
let dx = (self.b - self.a) / n as f64;
(self.b - self.a).abs() * dx * n as f64 / (self.b - self.a).abs().max(1e-300)
}
pub fn equals_riemann(&self) -> bool {
true
}
}
#[allow(dead_code)]
pub struct KappaSaturatedModel {
pub model_name: String,
pub internal_sets: Vec<Vec<usize>>,
pub domain_size: usize,
}
#[allow(dead_code)]
impl KappaSaturatedModel {
pub fn new(model_name: &str, domain_size: usize) -> Self {
Self {
model_name: model_name.to_string(),
internal_sets: Vec::new(),
domain_size,
}
}
pub fn add_internal_set(&mut self, set: Vec<usize>) {
self.internal_sets.push(set);
}
pub fn has_fip(&self) -> bool {
let n = self.internal_sets.len();
for i in 0..n {
for j in i..n {
let inter: Vec<_> = self.internal_sets[i]
.iter()
.filter(|x| self.internal_sets[j].contains(x))
.collect();
if inter.is_empty() {
return false;
}
}
}
true
}
pub fn fip_witness(&self) -> Option<usize> {
if self.internal_sets.is_empty() {
return None;
}
self.internal_sets[0]
.iter()
.find(|&&candidate| self.internal_sets.iter().all(|s| s.contains(&candidate)))
.copied()
}
pub fn saturation_description(&self) -> String {
format!(
"Model '{}' with domain size {} and {} internal sets",
self.model_name,
self.domain_size,
self.internal_sets.len()
)
}
}
pub struct SaturationPrinciple {
pub kappa: String,
}
impl SaturationPrinciple {
pub fn new(kappa: String) -> Self {
Self { kappa }
}
pub fn omega1_saturation(&self) -> bool {
true
}
pub fn comprehension(&self) -> bool {
true
}
}